MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  imbi12d Unicode version

Theorem imbi12d 312
Description: Deduction joining two equivalences to form equivalence of implications. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
imbi12d.1  |-  ( ph  ->  ( ps  <->  ch )
)
imbi12d.2  |-  ( ph  ->  ( th  <->  ta )
)
Assertion
Ref Expression
imbi12d  |-  ( ph  ->  ( ( ps  ->  th )  <->  ( ch  ->  ta ) ) )

Proof of Theorem imbi12d
StepHypRef Expression
1 imbi12d.1 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
21imbi1d 309 . 2  |-  ( ph  ->  ( ( ps  ->  th )  <->  ( ch  ->  th ) ) )
3 imbi12d.2 . . 3  |-  ( ph  ->  ( th  <->  ta )
)
43imbi2d 308 . 2  |-  ( ph  ->  ( ( ch  ->  th )  <->  ( ch  ->  ta ) ) )
52, 4bitrd 245 1  |-  ( ph  ->  ( ( ps  ->  th )  <->  ( ch  ->  ta ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177
This theorem is referenced by:  nfbidf  1786  drnf1  2026  drnf2  2027  equveliOLD  2043  ax11v2  2045  ax11vALT  2146  ax10-16  2240  ax11eq  2243  ax11el  2244  ax11inda  2250  ax11v2-o  2251  mobid  2288  2mo  2332  2eu6  2339  axext3  2387  ralcom2  2832  cbvralf  2886  cbvraldva2  2896  vtoclgaf  2976  vtocl2gaf  2978  vtocl3gaf  2980  rspct  3005  rspc  3006  ceqex  3026  ralab2  3059  mob2  3074  mob  3076  morex  3078  reu7  3089  reu8  3090  nelrdva  3103  cdeqim  3114  sbcimg  3162  csbhypf  3246  cbvralcsf  3271  dfss2f  3299  sbcss  3698  sneqrg  3928  elintab  4021  intss1  4025  intmin  4030  dfiin2g  4084  trel  4269  trss  4271  zfpow  4338  rext  4372  opth  4395  copsexg  4402  poeq1  4466  pocl  4470  swopolem  4472  swopo  4473  isso2i  4495  fri  4504  ordelord  4563  reusv2lem4  4686  reusv3i  4689  tfis  4793  tfisi  4797  tfindsg  4799  tfindsg2  4800  tfindes  4801  dfom2  4806  limomss  4809  nnlim  4817  findsg  4831  findes  4834  vtoclr  4881  poinxp  4900  posn  4905  ssrel  4923  ssrel2  4925  ssrelrel  4935  relop  4982  issref  5206  iota5  5397  funopg  5444  brprcneu  5680  tz6.12f  5708  funbrfv  5724  ssimaexg  5748  fvmptf  5780  fvelrn  5825  fprg  5874  f1veqaeq  5964  dff13f  5965  soisores  6006  soisoi  6007  isofrlem  6019  isopolem  6024  f1oweALT  6033  weniso  6034  oprabid  6064  ovmpt2s  6156  ov2gf  6157  ov3  6169  caovcan  6210  caovordig  6211  caofrss  6296  caoftrn  6298  dfoprab4f  6364  f1o2ndf1  6413  frxp  6415  poxp  6417  riota5f  6533  riotasv2d  6553  riotasv2dOLD  6554  onfununi  6562  smoel  6581  smogt  6588  tfrlem1  6595  tz7.48lem  6657  tz7.49  6661  oawordeu  6757  omordi  6768  oeordi  6789  nnmordi  6833  omabs  6849  nneob  6854  omsmolem  6855  qsel  6942  eroveu  6958  ecopovtrn  6966  th3qlem2  6970  ixpsnf1o  7061  fundmeng  7140  sbth  7186  limensuc  7243  nneneq  7249  php  7250  php2  7251  unxpdom  7275  pssnn  7286  findcard  7306  findcard2  7307  findcard3  7309  ac6sfi  7310  frfi  7311  domunfican  7338  fiint  7342  iunfi  7353  finsschain  7371  dffi3  7394  marypha1lem  7396  marypha1  7397  supmo  7413  suplub  7421  supisolem  7431  ordiso2  7440  ordtypelem7  7449  wemaplem1  7471  wemaplem2  7472  zfregcl  7518  inf0  7532  inf3lem1  7539  zfinf  7550  axinf2  7551  dfom3  7558  elom3  7559  cantnfval2  7580  cantnfle  7582  cantnflt  7583  cantnfp1lem3  7592  oemapvali  7596  cantnflem1c  7599  cantnflem1  7601  cantnf  7605  wemapwe  7610  cnfcom  7613  setind  7629  r1sdom  7656  r1ordg  7660  rankonidlem  7710  rankunb  7732  bnd2  7773  infxpenlem  7851  infxpenc2  7859  dfac8alem  7866  dfac8clem  7869  indcardi  7878  alephordi  7911  alephinit  7932  alephfp  7945  aceq3lem  7957  dfac5lem4  7963  dfac5  7965  dfac2  7967  dfac9  7972  dfac12lem2  7980  dfac12lem3  7981  kmlem1  7986  kmlem4  7989  kmlem10  7995  kmlem12  7997  kmlem13  7998  pwsdompw  8040  ackbij1lem16  8071  cfslb2n  8104  cfsmolem  8106  sornom  8113  fin2i  8131  infpssrlem4  8142  isfin2-2  8155  isfin3ds  8165  fin23lem17  8174  fin23lem32  8180  fin23lem34  8182  fin23lem35  8183  fin23lem39  8186  fin23lem41  8188  isf32lem2  8190  isf33lem  8202  isf34lem4  8213  isf34lem6  8216  fin1a2lem10  8245  axcc2lem  8272  axcc3  8274  axcc4dom  8277  dominf  8281  axdc2lem  8284  axdc3lem2  8287  ac6sg  8324  zorn2lem7  8338  zornn0g  8341  ttukeylem5  8349  ttukeylem6  8350  axdclem  8355  fodomg  8359  dominfac  8404  axrepndlem1  8423  axrepndlem2  8424  axunndlem1  8426  axunnd  8427  axpowndlem2  8429  axpowndlem3  8430  axpowndlem4  8431  axregndlem2  8434  axregnd  8435  axinfndlem1  8436  axinfnd  8437  axacndlem4  8441  axacndlem5  8442  axacnd  8443  zfcndpow  8447  zfcndinf  8449  fpwwe2lem5  8465  fpwwe2lem8  8468  fpwwe2lem12  8472  pwfseqlem4a  8492  pwfseqlem4  8493  pwfseqlem5  8494  pwfseq  8495  wunfi  8552  wunex2  8569  inar1  8606  rankcf  8608  tskord  8611  grudomon  8648  grur1a  8650  axgroth6  8659  axgroth3  8662  axgroth4  8663  eltskm  8674  indpi  8740  pinq  8760  nqereu  8762  prcdnq  8826  prnmax  8828  ltsopr  8865  prlem936  8880  ltsosr  8925  recexsrlem  8934  mulgt0sr  8936  map2psrpr  8941  supsrlem  8942  axrrecex  8994  axpre-lttrn  8997  axpre-mulgt0  8999  axpre-sup  9000  axsup  9107  ltordlem  9508  ltord1  9509  wloglei  9515  squeeze0  9869  infm3  9923  nnsub  9994  nnunb  10173  peano5uzti  10315  uzindOLD  10320  fzind  10324  eluzadd  10470  eluzsub  10471  uzind4s  10492  uzind4s2  10493  zmax  10527  zbtwnre  10528  xmulasslem  10820  xrsupsslem  10841  xrinfmsslem  10842  xrub  10846  injresinj  11155  om2uzlti  11245  uzindi  11275  axdc4uz  11277  seqp1  11293  seqcl2  11296  seqfveq2  11300  seqshft2  11304  monoord  11308  seqsplit  11311  seqf1olem2  11318  seqf1o  11319  seqid2  11324  seqhomo  11325  seqof2  11336  expcl2lem  11348  facdiv  11533  facwordi  11535  faclbnd4lem2  11540  hashnn0n0nn  11619  hashf1lem2  11660  seqcoll  11667  brfi1uzind  11670  wrdind  11746  rlim2  12245  ello1mpt  12270  rlimclim1  12294  o1co  12335  o1compt  12336  rlimcn1  12337  rlimcn2  12339  climcn1  12340  climcn2  12341  subcn2  12343  o1of2  12361  caucvgrlem  12421  fsum2d  12510  fsumabs  12535  fsumtscopo  12536  fsumrlim  12545  fsumo1  12546  o1fsum  12547  fsumiun  12555  rpnnen2lem10  12778  sqr2irr  12803  dvdsle  12850  divalglem7  12874  divalglem8  12875  ndvdssub  12882  gcdcllem1  12966  algcvg  13022  algcvga  13025  algfx  13026  isprm2lem  13041  prmind2  13045  dvdsprime  13047  nprm  13048  dvdsprm  13054  coprm  13055  coprmdvds2  13058  isprm6  13064  exprmfct  13065  prmfac1  13073  eulerthlem2  13126  pcqmul  13182  pcqcl  13185  pc2dvds  13207  pcz  13209  prmpwdvds  13227  infpn2  13236  vdwlem12  13315  ramub2  13337  rami  13338  ramcl  13352  prmlem0  13383  mreintcl  13775  ismred2  13783  mrissmrcd  13820  mreexexlemd  13824  iscatd2  13861  moni  13917  yoniso  14337  isprs  14342  prslem  14343  drsdirfi  14350  ispos  14359  posi  14362  isposd  14367  lubfval  14390  lubid  14394  glbfval  14395  joinle  14405  meetle  14412  isclat  14493  clatlem  14494  clatl  14498  lubl  14502  lubun  14505  clatleglb  14508  pospropd  14516  poslubmo  14528  ipodrsima  14546  acsdrsel  14548  isacs4lem  14549  isacs5lem  14550  acsdrscl  14551  mreclat  14568  pslem  14593  spwval2  14611  spwmo  14613  dirtr  14636  isnsg2  14925  ghmf1  14989  orbsta  15045  sylow1lem1  15187  sylow2alem2  15207  sylow2a  15208  lsmmod  15262  lsmdisj2  15269  efgsrel  15321  efgredlemd  15331  efgredlem  15334  efgred  15335  gsumzaddlem  15481  dprdval  15516  dprddisj2  15552  ablfac1eulem  15585  pgpfac1lem1  15587  pgpfac1lem5  15592  pgpfac1  15593  pgpfaclem2  15595  pgpfac  15597  irredmul  15769  isdrngrd  15816  islbs3  16182  rrgval  16302  rrgeq0i  16304  isdomn  16309  domneq0  16312  mplsubglem  16453  mpllsslem  16454  mplcoe1  16483  mplcoe2  16485  prmirredlem  16728  znfld  16796  znrrg  16801  cygznlem3  16805  isphl  16814  ipeq0  16824  isphld  16840  phlpropd  16841  lsmcss  16874  uniopn  16925  fiinopn  16929  epttop  17028  clsndisj  17094  elcls3  17102  neiptoptop  17150  neiptopnei  17151  cnpval  17254  iscnp  17255  cnpimaex  17274  lmcvg  17280  cnprest  17307  cnprest2  17308  lmss  17316  lmff  17319  ist1  17339  t0sep  17342  hausnei  17346  isnrm2  17376  t1sep2  17387  isreg2  17395  iscmp  17405  cmpcov  17406  cmpsublem  17416  cmpsub  17417  tgcmp  17418  uncmp  17420  fiuncmp  17421  hauscmplem  17423  cmpfi  17425  cmpfii  17426  dfcon2  17435  consuba  17436  connsub  17437  nconsubb  17439  1stcclb  17460  1stcfb  17461  2ndc1stc  17467  1stcrest  17469  1stcelcls  17477  restnlly  17498  lly1stc  17512  kgenval  17520  kgeni  17522  kgencn2  17542  ptcldmpt  17599  ptclsg  17600  dfac14lem  17602  dfac14  17603  txcnp  17605  ptcnp  17607  hausdiag  17630  txlm  17633  tx1stc  17635  xkococn  17645  cnmpt12  17652  cnmpt22  17659  kqt0lem  17721  isr0  17722  regr1lem2  17725  kqreglem1  17726  r0sep  17733  ptcmpfi  17798  elmptrab  17812  isfil  17832  filss  17838  isufil2  17893  cfinufil  17913  rnelfm  17938  fmfnfmlem2  17940  fmfnfmlem4  17942  flimopn  17960  flimrest  17968  flftg  17981  cnpflf  17986  txflf  17991  fclsopni  18000  fclsrest  18009  fclscf  18010  flimfnfcls  18013  fcfnei  18020  alexsublem  18028  alexsubb  18030  alexsubALTlem3  18033  alexsubALTlem4  18034  alexsubALT  18035  cnextcn  18051  cnextfres  18052  tgpt0  18101  divstgplem  18103  tsmsi  18116  tsmssubm  18125  tsmsres  18126  tsmsf1o  18127  tsmsxp  18137  ustssel  18188  ust0  18202  ustuqtop4  18227  ucnima  18264  ucncn  18268  iscusp  18282  cuspcvg  18284  imasdsf1olem  18356  blssps  18407  blss  18408  metss  18491  comet  18496  metcnp3  18523  metcnp2  18525  txmetcnp  18530  metuel2  18562  metucnOLD  18571  metucn  18572  nrmmetd  18575  nlmvscn  18676  nrginvrcn  18680  nmolb  18704  xrge0tsms  18818  divcn  18851  fsumcn  18853  elcncf2  18873  cncfi  18877  mulc1cncf  18888  cncfco  18890  cncfmet  18891  xrhmeo  18924  bndth  18936  nmoleub2lem2  19077  nmoleub3  19080  ipcn  19153  lmmbr  19164  caucfil  19189  pmltpc  19300  ovolfiniun  19350  ovolicc2lem3  19368  ovolicc2  19371  mblsplit  19381  finiunmbl  19391  volfiniun  19394  voliunlem3  19399  ioorinv  19421  ioorcl  19422  dyadmax  19443  dyadmbllem  19444  dyadmbl  19445  opnmbllem  19446  volcn  19451  vitalilem2  19454  vitalilem3  19455  vitali  19458  i1fd  19526  itg2seq  19587  itg2addlem  19603  itgfsum  19671  ellimc3  19719  dvbsss  19742  dvnres  19770  dvmptfsum  19812  dvferm1lem  19821  dvferm2lem  19823  rolle  19827  c1lip1  19834  lhop1lem  19850  lhop1  19851  dvfsumlem2  19864  dvfsumlem4  19866  dvfsumrlim  19868  dvfsum2  19871  ftc1a  19874  ftc1lem4  19876  ftc1lem6  19878  mpfind  19918  pf1ind  19928  mdegleb  19940  mdeglt  19941  deg1leb  19971  deg1lt  19973  ply1divex  20012  fta1glem2  20042  fta1g  20043  plyco0  20064  plyeq0lem  20082  coeeq2  20114  dgrle  20115  dgrcolem2  20145  dgrco  20146  plydivlem4  20166  plydivex  20167  fta1lem  20177  fta1  20178  vieta1lem2  20181  vieta1  20182  aalioulem2  20203  aalioulem4  20205  abelth  20310  cxpcn3  20585  rlimcnp  20757  xrlimcnp  20760  cxploglim  20769  scvxcvx  20777  jensen  20780  wilthlem2  20805  wilthlem3  20806  fta  20815  dvdsmulf1o  20932  perfectlem2  20967  dchrelbas3  20975  dchrelbas4  20980  dchrn0  20987  bcmono  21014  lgsdir2lem4  21063  lgsdchr  21085  lgseisenlem2  21087  lgsquad2lem2  21096  2sqlem6  21106  2sqlem8  21109  2sqlem10  21111  dchrisumlema  21135  dchrisumlem2  21137  dchrisumlem3  21138  wlkntrllem3  21514  1pthoncl  21545  2pthoncl  21556  fargshiftf1  21577  constr3trllem2  21591  eupatrl  21643  eupath2  21655  isass  21857  ismgm  21861  isexid2  21866  nvz  22111  nmobndseqi  22233  nmobndseqiOLD  22234  nmlno0  22249  blocnilem  22258  dipdir  22296  dipass  22299  siilem2  22306  ubthlem2  22326  ubth  22328  htth  22374  normpyth  22600  norm3lemt  22607  chlimi  22690  chcompl  22698  omlsii  22858  pjoml  22891  h1de2i  23008  elspansn2  23022  h1datom  23037  pjoml2  23066  pjoml3  23067  lecm  23072  chscllem2  23093  osum  23100  spansncv  23108  pjcjt2  23147  pjopyth  23175  eigre  23291  eigorth  23294  hhcno  23360  hhcnf  23361  cnopc  23369  cnfnc  23386  nmcexi  23482  nmcopexi  23483  nmcfnexi  23507  pjssge0i  23622  hstel2  23675  stj  23691  stri  23713  hstri  23721  stcltr1i  23730  mdbr  23750  mdi  23751  mdbr3  23753  mdbr4  23754  dmdbr  23755  dmdmd  23756  dmdi  23758  dmdbr3  23761  dmdbr4  23762  dmdbr5  23764  mdsl1i  23777  mdslmd1lem3  23783  mdslmd1lem4  23784  mdslmd1i  23785  csmdsymi  23790  cvmd  23792  atss  23802  atom1d  23809  chcv1  23811  hatomic  23816  atord  23844  atcvat2  23845  mddmdin0i  23887  rmoxfrdOLD  23932  rmoxfrd  23933  ifeqeqx  23954  ssiun2sf  23963  fmptcof2  24029  resspos  24140  toslub  24144  tosglb  24145  xrge0tsmsd  24176  isofld  24188  ofldadd  24191  ofldmul  24192  kerf1hrm  24215  xrge0iifiso  24274  esumcvg  24429  isrnsigaOLD  24448  sigaclcu  24453  sigaclci  24468  unelsiga  24470  measvun  24516  measiun  24525  sibfof  24607  sitgclg  24609  lgamgulmlem2  24767  subfacp1lem6  24824  erdszelem9  24838  kur14lem9  24853  sconpht  24869  cvmsss2  24914  cvmliftlem7  24931  cvmliftlem10  24934  ghomf1olem  25058  relexpsucr  25083  relexpsucl  25085  relexpcnv  25086  relexpdm  25088  relexprn  25089  relexpadd  25091  relexpindlem  25092  rtrclreclem.min  25100  iota5f  25135  dedekind  25140  prodfdiv  25177  fprod2d  25258  dfpo2  25326  fununiq  25340  setinds  25348  dfon2lem3  25355  dfon2lem4  25356  dfon2lem5  25357  dfon2lem6  25358  dfon2lem7  25359  dfon2lem8  25360  dfon2  25362  predbrg  25400  preddowncl  25410  tfisg  25418  wfisg  25423  frmin  25456  frinsg  25459  wfrlem9  25478  frrlem5e  25503  nocvxminlem  25558  axcgrtr  25758  btwnconn1lem11  25935  linethru  25991  rankelg  26013  rankeq1o  26016  mblfinlem  26143  mblfinlem2  26144  voliunnfl  26149  volsupnfl  26150  mbfresfi  26152  itg2addnclem3  26157  itg2gt0cn  26159  ftc1cnnclem  26177  ftc1cnnc  26178  subtr  26207  subtr2  26208  trer  26209  nn0prpwlem  26215  nn0prpw  26216  comppfsc  26277  neibastop2lem  26279  filnetlem4  26300  f1opr  26316  sdclem2  26336  fdc  26339  fdc1  26340  neificl  26349  mettrifi  26353  sstotbnd2  26373  cntotbnd  26395  heibor1lem  26408  bfp  26423  iscringd  26499  ispridl  26534  pridl  26537  ismaxidl  26540  maxidlmax  26543  ispridlc  26570  pridlc  26571  dmnnzd  26575  ismrcd1  26642  ismrcd2  26643  ismrc  26645  isnacs3  26654  nacsfix  26656  mzpcompact2  26699  fphpd  26767  fphpdo  26768  monotuz  26894  monotoddzzfi  26895  monotoddzz  26896  oddcomabszz  26897  zindbi  26899  setindtrs  26986  dford3lem2  26988  ttac  26997  dnnumch1  27009  fnwe2lem2  27016  aomclem3  27021  aomclem6  27024  supeq123d  27026  aomclem8  27027  dfac11  27028  dfac21  27032  islssfg2  27037  frlmup1  27118  lindfrn  27159  islindf4  27176  islindf5  27177  hbtlem5  27200  hbt  27202  flcidc  27247  symggen  27279  psgnunilem4  27288  mendlmod  27369  sdrgacs  27377  pm14.122b  27491  sbiota1  27502  fnchoice  27567  fmul01  27577  fmulcl  27578  fmuldfeqlem1  27579  fmuldfeq  27580  fmul01lt1lem1  27581  fmul01lt1lem2  27582  climmulf  27597  climexp  27598  climsuse  27601  climrecf  27602  climinff  27604  stoweidlem3  27619  stoweidlem4  27620  stoweidlem6  27622  stoweidlem8  27624  stoweidlem15  27631  stoweidlem16  27632  stoweidlem17  27633  stoweidlem19  27635  stoweidlem20  27636  stoweidlem22  27638  stoweidlem23  27639  stoweidlem26  27642  stoweidlem27  27643  stoweidlem30  27646  stoweidlem31  27647  stoweidlem32  27648  stoweidlem34  27650  stoweidlem35  27651  stoweidlem42  27658  stoweidlem43  27659  stoweidlem48  27664  stoweidlem50  27666  stoweidlem51  27667  stoweidlem57  27673  stoweidlem59  27675  stoweidlem62  27678  wallispilem3  27683  sbcfun  27854  swrdccatin1  28016  swrdccatin2  28018  swrdccatin12b  28027  swrdccatin12c  28028  swrdccat3  28029  usgra2pthspth  28035  usgra2wlkspthlem1  28036  usgra2wlkspthlem2  28037  usgra2pthlem1  28040  frgra3vlem1  28104  3vfriswmgralem  28108  3vfriswmgra  28109  frgrawopreglem4  28150  frg2wot1  28160  frg2woteqm  28162  usg2spot2nb  28168  imbi12  28314  sbcssOLD  28338  bnj1385  28910  bnj110  28935  bnj222  28960  bnj229  28961  bnj590  28987  bnj865  29000  bnj849  29002  bnj981  29027  bnj1014  29037  bnj1015  29038  bnj1112  29058  bnj1118  29059  bnj1123  29061  bnj1128  29065  bnj1125  29067  bnj1148  29071  bnj1154  29074  bnj1326  29101  bnj1384  29107  bnj1489  29131  bnj1497  29135  drnf1NEW7  29201  drnf2wAUX7  29204  drnf2w2AUX7  29207  drnf2w3AUX7  29210  equveliNEW7  29232  ax11v2NEW7  29234  drnf2OLD7  29400  lubunNEW  29456  lshpdisj  29470  lsmsatcv  29493  lsat0cv  29516  lcvexchlem4  29520  lcvexchlem5  29521  l1cvpat  29537  isopos  29663  oposlem  29666  isoml  29721  omllaw  29726  isatl  29782  atlex  29799  iscvlat  29806  cvlexch1  29811  glbconN  29859  hlsuprexch  29863  ps-1  29959  3atlem5  29969  psubspi  30229  llnexchb2  30351  elpcliN  30375  pclfinclN  30432  ldilval  30595  ltrnfset  30599  ltrnset  30600  ltrnu  30603  trlfset  30642  trlset  30643  trlval2  30645  cdleme25cv  30840  cdleme31so  30861  cdleme31fv  30872  cdlemefrs29bpre0  30878  cdleme32fva  30919  cdleme40v  30951  trlord  31051  cdlemkid3N  31415  cdlemkid4  31416  dihffval  31713  dihfval  31714  dihval  31715  lpolconN  31970  mapdordlem2  32120  hdmapfval  32313  hdmapval  32314  hdmapval2  32318
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178
  Copyright terms: Public domain W3C validator