MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  imbi12d Structured version   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  1790  drnf1  2057  drnf2OLD  2059  ax11v2  2074  ax11v2OLD  2075  equveliOLD  2082  ax11vALT  2172  ax10-16  2266  ax11eq  2269  ax11el  2270  ax11inda  2276  ax11v2-o  2277  mobid  2314  2mo  2358  2eu6  2365  axext3  2418  ralcom2  2864  cbvralf  2918  cbvraldva2  2928  vtoclgaf  3008  vtocl2gaf  3010  vtocl3gaf  3012  rspct  3037  rspc  3038  ceqex  3058  ralab2  3091  mob2  3106  mob  3108  morex  3110  reu7  3121  reu8  3122  nelrdva  3135  cdeqim  3146  sbcimg  3194  csbhypf  3278  cbvralcsf  3303  dfss2f  3331  sbcss  3730  sneqrg  3960  elintab  4053  intss1  4057  intmin  4062  dfiin2g  4116  trel  4301  trss  4303  zfpow  4370  rext  4404  opth  4427  copsexg  4434  poeq1  4498  pocl  4502  swopolem  4504  swopo  4505  isso2i  4527  fri  4536  ordelord  4595  reusv2lem4  4719  reusv3i  4722  tfis  4826  tfisi  4830  tfindsg  4832  tfindsg2  4833  tfindes  4834  dfom2  4839  limomss  4842  nnlim  4850  findsg  4864  findes  4867  vtoclr  4914  poinxp  4933  posn  4938  ssrel  4956  ssrel2  4958  ssrelrel  4968  relop  5015  issref  5239  iota5  5430  funopg  5477  brprcneu  5713  tz6.12f  5741  funbrfv  5757  ssimaexg  5781  fvmptf  5813  fvelrn  5858  fprg  5907  f1veqaeq  5997  dff13f  5998  soisores  6039  soisoi  6040  isofrlem  6052  isopolem  6057  f1oweALT  6066  weniso  6067  oprabid  6097  ovmpt2s  6189  ov2gf  6190  ov3  6202  caovcan  6243  caovordig  6244  caofrss  6329  caoftrn  6331  dfoprab4f  6397  f1o2ndf1  6446  frxp  6448  poxp  6450  riota5f  6566  riotasv2d  6586  riotasv2dOLD  6587  onfununi  6595  smoel  6614  smogt  6621  tfrlem1  6628  tz7.48lem  6690  tz7.49  6694  oawordeu  6790  omordi  6801  oeordi  6822  nnmordi  6866  omabs  6882  nneob  6887  omsmolem  6888  qsel  6975  eroveu  6991  ecopovtrn  6999  th3qlem2  7003  ixpsnf1o  7094  fundmeng  7173  sbth  7219  limensuc  7276  nneneq  7282  php  7283  php2  7284  unxpdom  7308  pssnn  7319  findcard  7339  findcard2  7340  findcard3  7342  ac6sfi  7343  frfi  7344  domunfican  7371  fiint  7375  iunfi  7386  finsschain  7405  dffi3  7428  marypha1lem  7430  marypha1  7431  supeq3  7446  supeq123d  7447  supmo  7449  suplub  7457  supisolem  7467  ordiso2  7476  ordtypelem7  7485  wemaplem1  7507  wemaplem2  7508  zfregcl  7554  inf0  7568  inf3lem1  7575  zfinf  7586  axinf2  7587  dfom3  7594  elom3  7595  cantnfval2  7616  cantnfle  7618  cantnflt  7619  cantnfp1lem3  7628  oemapvali  7632  cantnflem1c  7635  cantnflem1  7637  cantnf  7641  wemapwe  7646  cnfcom  7649  setind  7665  r1sdom  7692  r1ordg  7696  rankonidlem  7746  rankunb  7768  bnd2  7809  infxpenlem  7887  infxpenc2  7895  dfac8alem  7902  dfac8clem  7905  indcardi  7914  alephordi  7947  alephinit  7968  alephfp  7981  aceq3lem  7993  dfac5lem4  7999  dfac5  8001  dfac2  8003  dfac9  8008  dfac12lem2  8016  dfac12lem3  8017  kmlem1  8022  kmlem4  8025  kmlem10  8031  kmlem12  8033  kmlem13  8034  pwsdompw  8076  ackbij1lem16  8107  cfslb2n  8140  cfsmolem  8142  sornom  8149  fin2i  8167  infpssrlem4  8178  isfin2-2  8191  isfin3ds  8201  fin23lem17  8210  fin23lem32  8216  fin23lem34  8218  fin23lem35  8219  fin23lem39  8222  fin23lem41  8224  isf32lem2  8226  isf33lem  8238  isf34lem4  8249  isf34lem6  8252  fin1a2lem10  8281  axcc2lem  8308  axcc3  8310  axcc4dom  8313  dominf  8317  axdc2lem  8320  axdc3lem2  8323  ac6sg  8360  zorn2lem7  8374  zornn0g  8377  ttukeylem5  8385  ttukeylem6  8386  axdclem  8391  fodomg  8395  dominfac  8440  axrepndlem1  8459  axrepndlem2  8460  axunndlem1  8462  axunnd  8463  axpowndlem2  8465  axpowndlem3  8466  axpowndlem4  8467  axregndlem2  8470  axregnd  8471  axinfndlem1  8472  axinfnd  8473  axacndlem4  8477  axacndlem5  8478  axacnd  8479  zfcndpow  8483  zfcndinf  8485  fpwwe2lem5  8501  fpwwe2lem8  8504  fpwwe2lem12  8508  pwfseqlem4a  8528  pwfseqlem4  8529  pwfseqlem5  8530  pwfseq  8531  wunfi  8588  wunex2  8605  inar1  8642  rankcf  8644  tskord  8647  grudomon  8684  grur1a  8686  axgroth6  8695  axgroth3  8698  axgroth4  8699  eltskm  8710  indpi  8776  pinq  8796  nqereu  8798  prcdnq  8862  prnmax  8864  ltsopr  8901  prlem936  8916  ltsosr  8961  recexsrlem  8970  mulgt0sr  8972  map2psrpr  8977  supsrlem  8978  axrrecex  9030  axpre-lttrn  9033  axpre-mulgt0  9035  axpre-sup  9036  axsup  9143  ltordlem  9544  ltord1  9545  wloglei  9551  squeeze0  9905  infm3  9959  nnsub  10030  nnunb  10209  peano5uzti  10351  uzindOLD  10356  fzind  10360  eluzadd  10506  eluzsub  10507  uzind4s  10528  uzind4s2  10529  zmax  10563  zbtwnre  10564  xmulasslem  10856  xrsupsslem  10877  xrinfmsslem  10878  xrub  10882  injresinj  11192  om2uzlti  11282  uzindi  11312  axdc4uz  11314  seqp1  11330  seqcl2  11333  seqfveq2  11337  seqshft2  11341  monoord  11345  seqsplit  11348  seqf1olem2  11355  seqf1o  11356  seqid2  11361  seqhomo  11362  seqof2  11373  expcl2lem  11385  facdiv  11570  facwordi  11572  faclbnd4lem2  11577  hashnn0n0nn  11656  hashf1lem2  11697  seqcoll  11704  brfi1uzind  11707  wrdind  11783  rlim2  12282  ello1mpt  12307  rlimclim1  12331  o1co  12372  o1compt  12373  rlimcn1  12374  rlimcn2  12376  climcn1  12377  climcn2  12378  subcn2  12380  o1of2  12398  caucvgrlem  12458  fsum2d  12547  fsumabs  12572  fsumtscopo  12573  fsumrlim  12582  fsumo1  12583  o1fsum  12584  fsumiun  12592  rpnnen2lem10  12815  sqr2irr  12840  dvdsle  12887  divalglem7  12911  divalglem8  12912  ndvdssub  12919  gcdcllem1  13003  algcvg  13059  algcvga  13062  algfx  13063  isprm2lem  13078  prmind2  13082  dvdsprime  13084  nprm  13085  dvdsprm  13091  coprm  13092  coprmdvds2  13095  isprm6  13101  exprmfct  13102  prmfac1  13110  eulerthlem2  13163  pcqmul  13219  pcqcl  13222  pc2dvds  13244  pcz  13246  prmpwdvds  13264  infpn2  13273  vdwlem12  13352  ramub2  13374  rami  13375  ramcl  13389  prmlem0  13420  mreintcl  13812  ismred2  13820  mrissmrcd  13857  mreexexlemd  13861  iscatd2  13898  moni  13954  yoniso  14374  isprs  14379  prslem  14380  drsdirfi  14387  ispos  14396  posi  14399  isposd  14404  lubfval  14427  lubid  14431  glbfval  14432  joinle  14442  meetle  14449  isclat  14530  clatlem  14531  clatl  14535  lubl  14539  lubun  14542  clatleglb  14545  pospropd  14553  poslubmo  14565  ipodrsima  14583  acsdrsel  14585  isacs4lem  14586  isacs5lem  14587  acsdrscl  14588  mreclat  14605  pslem  14630  spwval2  14648  spwmo  14650  dirtr  14673  isnsg2  14962  ghmf1  15026  orbsta  15082  sylow1lem1  15224  sylow2alem2  15244  sylow2a  15245  lsmmod  15299  lsmdisj2  15306  efgsrel  15358  efgredlemd  15368  efgredlem  15371  efgred  15372  gsumzaddlem  15518  dprdval  15553  dprddisj2  15589  ablfac1eulem  15622  pgpfac1lem1  15624  pgpfac1lem5  15629  pgpfac1  15630  pgpfaclem2  15632  pgpfac  15634  irredmul  15806  isdrngrd  15853  islbs3  16219  rrgval  16339  rrgeq0i  16341  isdomn  16346  domneq0  16349  mplsubglem  16490  mpllsslem  16491  mplcoe1  16520  mplcoe2  16522  prmirredlem  16765  znfld  16833  znrrg  16838  cygznlem3  16842  isphl  16851  ipeq0  16861  isphld  16877  phlpropd  16878  lsmcss  16911  uniopn  16962  fiinopn  16966  epttop  17065  clsndisj  17131  elcls3  17139  neiptoptop  17187  neiptopnei  17188  cnpval  17292  iscnp  17293  cnpimaex  17312  lmcvg  17318  cnprest  17345  cnprest2  17346  lmss  17354  lmff  17357  ist1  17377  t0sep  17380  hausnei  17384  isnrm2  17414  t1sep2  17425  isreg2  17433  iscmp  17443  cmpcov  17444  cmpsublem  17454  cmpsub  17455  tgcmp  17456  uncmp  17458  fiuncmp  17459  hauscmplem  17461  cmpfi  17463  cmpfii  17464  bwth  17465  dfcon2  17474  consuba  17475  connsub  17476  nconsubb  17478  1stcclb  17499  1stcfb  17500  2ndc1stc  17506  1stcrest  17508  1stcelcls  17516  restnlly  17537  lly1stc  17551  kgenval  17559  kgeni  17561  kgencn2  17581  ptcldmpt  17638  ptclsg  17639  dfac14lem  17641  dfac14  17642  txcnp  17644  ptcnp  17646  hausdiag  17669  txlm  17672  tx1stc  17674  xkococn  17684  cnmpt12  17691  cnmpt22  17698  kqt0lem  17760  isr0  17761  regr1lem2  17764  kqreglem1  17765  r0sep  17772  ptcmpfi  17837  elmptrab  17851  isfil  17871  filss  17877  isufil2  17932  cfinufil  17952  rnelfm  17977  fmfnfmlem2  17979  fmfnfmlem4  17981  flimopn  17999  flimrest  18007  flftg  18020  cnpflf  18025  txflf  18030  fclsopni  18039  fclsrest  18048  fclscf  18049  flimfnfcls  18052  fcfnei  18059  alexsublem  18067  alexsubb  18069  alexsubALTlem3  18072  alexsubALTlem4  18073  alexsubALT  18074  cnextcn  18090  cnextfres  18091  tgpt0  18140  divstgplem  18142  tsmsi  18155  tsmssubm  18164  tsmsres  18165  tsmsf1o  18166  tsmsxp  18176  ustssel  18227  ust0  18241  ustuqtop4  18266  ucnima  18303  ucncn  18307  iscusp  18321  cuspcvg  18323  imasdsf1olem  18395  blssps  18446  blss  18447  metss  18530  comet  18535  metcnp3  18562  metcnp2  18564  txmetcnp  18569  metuel2  18601  metucnOLD  18610  metucn  18611  nrmmetd  18614  nlmvscn  18715  nrginvrcn  18719  nmolb  18743  xrge0tsms  18857  divcn  18890  fsumcn  18892  elcncf2  18912  cncfi  18916  mulc1cncf  18927  cncfco  18929  cncfmet  18930  xrhmeo  18963  bndth  18975  nmoleub2lem2  19116  nmoleub3  19119  ipcn  19192  lmmbr  19203  caucfil  19228  pmltpc  19339  ovolfiniun  19389  ovolicc2lem3  19407  ovolicc2  19410  mblsplit  19420  finiunmbl  19430  volfiniun  19433  voliunlem3  19438  ioorinv  19460  ioorcl  19461  dyadmax  19482  dyadmbllem  19483  dyadmbl  19484  opnmbllem  19485  volcn  19490  vitalilem2  19493  vitalilem3  19494  vitali  19497  i1fd  19565  itg2seq  19626  itg2addlem  19642  itgfsum  19710  ellimc3  19758  dvbsss  19781  dvnres  19809  dvmptfsum  19851  dvferm1lem  19860  dvferm2lem  19862  rolle  19866  c1lip1  19873  lhop1lem  19889  lhop1  19890  dvfsumlem2  19903  dvfsumlem4  19905  dvfsumrlim  19907  dvfsum2  19910  ftc1a  19913  ftc1lem4  19915  ftc1lem6  19917  mpfind  19957  pf1ind  19967  mdegleb  19979  mdeglt  19980  deg1leb  20010  deg1lt  20012  ply1divex  20051  fta1glem2  20081  fta1g  20082  plyco0  20103  plyeq0lem  20121  coeeq2  20153  dgrle  20154  dgrcolem2  20184  dgrco  20185  plydivlem4  20205  plydivex  20206  fta1lem  20216  fta1  20217  vieta1lem2  20220  vieta1  20221  aalioulem2  20242  aalioulem4  20244  abelth  20349  cxpcn3  20624  rlimcnp  20796  xrlimcnp  20799  cxploglim  20808  scvxcvx  20816  jensen  20819  wilthlem2  20844  wilthlem3  20845  fta  20854  dvdsmulf1o  20971  perfectlem2  21006  dchrelbas3  21014  dchrelbas4  21019  dchrn0  21026  bcmono  21053  lgsdir2lem4  21102  lgsdchr  21124  lgseisenlem2  21126  lgsquad2lem2  21135  2sqlem6  21145  2sqlem8  21148  2sqlem10  21150  dchrisumlema  21174  dchrisumlem2  21176  dchrisumlem3  21177  wlkntrllem3  21553  1pthoncl  21584  2pthoncl  21595  fargshiftf1  21616  constr3trllem2  21630  eupatrl  21682  eupath2  21694  isass  21896  ismgm  21900  isexid2  21905  nvz  22150  nmobndseqi  22272  nmobndseqiOLD  22273  nmlno0  22288  blocnilem  22297  dipdir  22335  dipass  22338  siilem2  22345  ubthlem2  22365  ubth  22367  htth  22413  normpyth  22639  norm3lemt  22646  chlimi  22729  chcompl  22737  omlsii  22897  pjoml  22930  h1de2i  23047  elspansn2  23061  h1datom  23076  pjoml2  23105  pjoml3  23106  lecm  23111  chscllem2  23132  osum  23139  spansncv  23147  pjcjt2  23186  pjopyth  23214  eigre  23330  eigorth  23333  hhcno  23399  hhcnf  23400  cnopc  23408  cnfnc  23425  nmcexi  23521  nmcopexi  23522  nmcfnexi  23546  pjssge0i  23661  hstel2  23714  stj  23730  stri  23752  hstri  23760  stcltr1i  23769  mdbr  23789  mdi  23790  mdbr3  23792  mdbr4  23793  dmdbr  23794  dmdmd  23795  dmdi  23797  dmdbr3  23800  dmdbr4  23801  dmdbr5  23803  mdsl1i  23816  mdslmd1lem3  23822  mdslmd1lem4  23823  mdslmd1i  23824  csmdsymi  23829  cvmd  23831  atss  23841  atom1d  23848  chcv1  23850  hatomic  23855  atord  23883  atcvat2  23884  mddmdin0i  23926  rmoxfrdOLD  23971  rmoxfrd  23972  ifeqeqx  23993  ssiun2sf  24002  fmptcof2  24068  resspos  24179  toslub  24183  tosglb  24184  xrge0tsmsd  24215  isofld  24227  ofldadd  24230  ofldmul  24231  kerf1hrm  24254  xrge0iifiso  24313  esumcvg  24468  isrnsigaOLD  24487  sigaclcu  24492  sigaclci  24507  unelsiga  24509  measvun  24555  measiun  24564  sibfof  24646  sitgclg  24648  lgamgulmlem2  24806  subfacp1lem6  24863  erdszelem9  24877  kur14lem9  24892  sconpht  24908  cvmsss2  24953  cvmliftlem7  24970  cvmliftlem10  24973  ghomf1olem  25097  relexpsucr  25122  relexpsucl  25124  relexpcnv  25125  relexpdm  25127  relexprn  25128  relexpadd  25130  relexpindlem  25131  rtrclreclem.min  25139  iota5f  25174  dedekind  25179  prodfdiv  25216  fprod2d  25297  dfpo2  25370  fununiq  25386  setinds  25397  dfon2lem3  25404  dfon2lem4  25405  dfon2lem5  25406  dfon2lem6  25407  dfon2lem7  25408  dfon2lem8  25409  dfon2  25411  predbrg  25453  preddowncl  25463  tfisg  25471  wfisg  25476  frmin  25509  frinsg  25512  wfrlem9  25538  frrlem5e  25582  nocvxminlem  25637  axcgrtr  25846  btwnconn1lem11  26023  linethru  26079  rankelg  26101  rankeq1o  26104  mblfinlem  26234  mblfinlem2  26235  voliunnfl  26240  volsupnfl  26241  mbfresfi  26243  itg2addnclem3  26248  itg2gt0cn  26250  ftc1cnnclem  26268  ftc1cnnc  26269  ftc1anclem7  26276  ftc1anc  26278  subtr  26308  subtr2  26309  trer  26310  nn0prpwlem  26316  nn0prpw  26317  comppfsc  26378  neibastop2lem  26380  filnetlem4  26401  f1opr  26417  sdclem2  26437  fdc  26440  fdc1  26441  neificl  26450  mettrifi  26454  sstotbnd2  26474  cntotbnd  26496  heibor1lem  26509  bfp  26524  iscringd  26600  ispridl  26635  pridl  26638  ismaxidl  26641  maxidlmax  26644  ispridlc  26671  pridlc  26672  dmnnzd  26676  ismrcd1  26743  ismrcd2  26744  ismrc  26746  isnacs3  26755  nacsfix  26757  mzpcompact2  26800  fphpd  26868  fphpdo  26869  monotuz  26995  monotoddzzfi  26996  monotoddzz  26997  oddcomabszz  26998  zindbi  27000  setindtrs  27087  dford3lem2  27089  ttac  27098  dnnumch1  27110  fnwe2lem2  27117  aomclem3  27122  aomclem6  27125  aomclem8  27127  dfac11  27128  dfac21  27132  islssfg2  27137  frlmup1  27218  lindfrn  27259  islindf4  27276  islindf5  27277  hbtlem5  27300  hbt  27302  flcidc  27347  symggen  27379  psgnunilem4  27388  mendlmod  27469  sdrgacs  27477  pm14.122b  27591  sbiota1  27602  fnchoice  27667  fmul01  27677  fmulcl  27678  fmuldfeqlem1  27679  fmuldfeq  27680  fmul01lt1lem1  27681  fmul01lt1lem2  27682  climmulf  27697  climexp  27698  climsuse  27701  climrecf  27702  climinff  27704  stoweidlem3  27719  stoweidlem4  27720  stoweidlem6  27722  stoweidlem8  27724  stoweidlem15  27731  stoweidlem16  27732  stoweidlem17  27733  stoweidlem19  27735  stoweidlem20  27736  stoweidlem22  27738  stoweidlem23  27739  stoweidlem26  27742  stoweidlem27  27743  stoweidlem30  27746  stoweidlem31  27747  stoweidlem32  27748  stoweidlem34  27750  stoweidlem35  27751  stoweidlem42  27758  stoweidlem43  27759  stoweidlem48  27764  stoweidlem50  27766  stoweidlem51  27767  stoweidlem57  27773  stoweidlem59  27775  stoweidlem62  27778  wallispilem3  27783  sbcfun  27954  swrdccatin1  28171  swrdccat3blem  28184  usgra2pthspth  28258  usgra2wlkspthlem1  28259  usgra2wlkspthlem2  28260  usgra2pthlem1  28263  frgra3vlem1  28327  3vfriswmgralem  28331  3vfriswmgra  28332  frgrawopreglem4  28373  frg2wot1  28383  frg2woteqm  28385  usg2spot2nb  28391  imbi12  28540  sbcssOLD  28564  bnj1385  29141  bnj110  29166  bnj222  29191  bnj229  29192  bnj590  29218  bnj865  29231  bnj849  29233  bnj981  29258  bnj1014  29268  bnj1015  29269  bnj1112  29289  bnj1118  29290  bnj1123  29292  bnj1128  29296  bnj1125  29298  bnj1148  29302  bnj1154  29305  bnj1326  29332  bnj1384  29338  bnj1489  29362  bnj1497  29366  drnf1NEW7  29432  drnf2wAUX7  29435  drnf2w2AUX7  29438  drnf2w3AUX7  29441  equveliNEW7  29465  ax11v2NEW7  29467  drnf2OLD7  29653  lubunNEW  29708  lshpdisj  29722  lsmsatcv  29745  lsat0cv  29768  lcvexchlem4  29772  lcvexchlem5  29773  l1cvpat  29789  isopos  29915  oposlem  29918  isoml  29973  omllaw  29978  isatl  30034  atlex  30051  iscvlat  30058  cvlexch1  30063  glbconN  30111  hlsuprexch  30115  ps-1  30211  3atlem5  30221  psubspi  30481  llnexchb2  30603  elpcliN  30627  pclfinclN  30684  ldilval  30847  ltrnfset  30851  ltrnset  30852  ltrnu  30855  trlfset  30894  trlset  30895  trlval2  30897  cdleme25cv  31092  cdleme31so  31113  cdleme31fv  31124  cdlemefrs29bpre0  31130  cdleme32fva  31171  cdleme40v  31203  trlord  31303  cdlemkid3N  31667  cdlemkid4  31668  dihffval  31965  dihfval  31966  dihval  31967  lpolconN  32222  mapdordlem2  32372  hdmapfval  32565  hdmapval  32566  hdmapval2  32570
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