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

Theorem imbi12d 313
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 310 . 2  |-  ( ph  ->  ( ( ps  ->  th )  <->  ( ch  ->  th ) ) )
3 imbi12d.2 . . 3  |-  ( ph  ->  ( th  <->  ta )
)
43imbi2d 309 . 2  |-  ( ph  ->  ( ( ch  ->  th )  <->  ( ch  ->  ta ) ) )
52, 4bitrd 246 1  |-  ( ph  ->  ( ( ps  ->  th )  <->  ( ch  ->  ta ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178
This theorem is referenced by:  nfbidf  1791  drnf1  2062  drnf2OLD  2064  ax11v2  2079  ax11v2OLD  2080  equveliOLD  2087  ax11vALT  2175  ax10-16  2269  ax11eq  2272  ax11el  2273  ax11inda  2279  ax11v2-o  2280  mobid  2317  2mo  2361  2eu6  2368  axext3  2421  ralcom2  2874  cbvralf  2928  cbvraldva2  2938  vtoclgaf  3018  vtocl2gaf  3020  vtocl3gaf  3022  rspct  3047  rspc  3048  ceqex  3068  ralab2  3101  mob2  3116  mob  3118  morex  3120  reu7  3131  reu8  3132  nelrdva  3145  cdeqim  3156  sbcimg  3204  csbhypf  3288  cbvralcsf  3313  dfss2f  3341  sbcss  3740  sneqrg  3970  elintab  4063  intss1  4067  intmin  4072  dfiin2g  4126  trel  4312  trss  4314  zfpow  4381  rext  4415  opth  4438  copsexg  4445  poeq1  4509  pocl  4513  swopolem  4515  swopo  4516  isso2i  4538  fri  4547  ordelord  4606  reusv2lem4  4730  reusv3i  4733  tfis  4837  tfisi  4841  tfindsg  4843  tfindsg2  4844  tfindes  4845  dfom2  4850  limomss  4853  nnlim  4861  findsg  4875  findes  4878  vtoclr  4925  poinxp  4944  posn  4949  ssrel  4967  ssrel2  4969  ssrelrel  4979  relop  5026  issref  5250  iota5  5441  funopg  5488  brprcneu  5724  tz6.12f  5752  funbrfv  5768  ssimaexg  5792  fvmptf  5824  fvelrn  5869  fprg  5918  f1veqaeq  6008  dff13f  6009  soisores  6050  soisoi  6051  isofrlem  6063  isopolem  6068  f1oweALT  6077  weniso  6078  oprabid  6108  ovmpt2s  6200  ov2gf  6201  ov3  6213  caovcan  6254  caovordig  6255  caofrss  6340  caoftrn  6342  dfoprab4f  6408  f1o2ndf1  6457  frxp  6459  poxp  6461  riota5f  6577  riotasv2d  6597  riotasv2dOLD  6598  onfununi  6606  smoel  6625  smogt  6632  tfrlem1  6639  tz7.48lem  6701  tz7.49  6705  oawordeu  6801  omordi  6812  oeordi  6833  nnmordi  6877  omabs  6893  nneob  6898  omsmolem  6899  qsel  6986  eroveu  7002  ecopovtrn  7010  th3qlem2  7014  ixpsnf1o  7105  fundmeng  7184  sbth  7230  limensuc  7287  nneneq  7293  php  7294  php2  7295  unxpdom  7319  pssnn  7330  findcard  7350  findcard2  7351  findcard3  7353  ac6sfi  7354  frfi  7355  domunfican  7382  fiint  7386  iunfi  7397  finsschain  7416  dffi3  7439  marypha1lem  7441  marypha1  7442  supeq3  7457  supeq123d  7458  supmo  7460  suplub  7468  supisolem  7478  ordiso2  7487  ordtypelem7  7496  wemaplem1  7518  wemaplem2  7519  zfregcl  7565  inf0  7579  inf3lem1  7586  zfinf  7597  axinf2  7598  dfom3  7605  elom3  7606  cantnfval2  7627  cantnfle  7629  cantnflt  7630  cantnfp1lem3  7639  oemapvali  7643  cantnflem1c  7646  cantnflem1  7648  cantnf  7652  wemapwe  7657  cnfcom  7660  setind  7676  r1sdom  7703  r1ordg  7707  rankonidlem  7757  rankunb  7779  bnd2  7822  infxpenlem  7900  infxpenc2  7908  dfac8alem  7915  dfac8clem  7918  indcardi  7927  alephordi  7960  alephinit  7981  alephfp  7994  aceq3lem  8006  dfac5lem4  8012  dfac5  8014  dfac2  8016  dfac9  8021  dfac12lem2  8029  dfac12lem3  8030  kmlem1  8035  kmlem4  8038  kmlem10  8044  kmlem12  8046  kmlem13  8047  pwsdompw  8089  ackbij1lem16  8120  cfslb2n  8153  cfsmolem  8155  sornom  8162  fin2i  8180  infpssrlem4  8191  isfin2-2  8204  isfin3ds  8214  fin23lem17  8223  fin23lem32  8229  fin23lem34  8231  fin23lem35  8232  fin23lem39  8235  fin23lem41  8237  isf32lem2  8239  isf33lem  8251  isf34lem4  8262  isf34lem6  8265  fin1a2lem10  8294  axcc2lem  8321  axcc3  8323  axcc4dom  8326  dominf  8330  axdc2lem  8333  axdc3lem2  8336  ac6sg  8373  zorn2lem7  8387  zornn0g  8390  ttukeylem5  8398  ttukeylem6  8399  axdclem  8404  fodomg  8408  dominfac  8453  axrepndlem1  8472  axrepndlem2  8473  axunndlem1  8475  axunnd  8476  axpowndlem2  8478  axpowndlem3  8479  axpowndlem4  8480  axregndlem2  8483  axregnd  8484  axinfndlem1  8485  axinfnd  8486  axacndlem4  8490  axacndlem5  8491  axacnd  8492  zfcndpow  8496  zfcndinf  8498  fpwwe2lem5  8514  fpwwe2lem8  8517  fpwwe2lem12  8521  pwfseqlem4a  8541  pwfseqlem4  8542  pwfseqlem5  8543  pwfseq  8544  wunfi  8601  wunex2  8618  inar1  8655  rankcf  8657  tskord  8660  grudomon  8697  grur1a  8699  axgroth6  8708  axgroth3  8711  axgroth4  8712  eltskm  8723  indpi  8789  pinq  8809  nqereu  8811  prcdnq  8875  prnmax  8877  ltsopr  8914  prlem936  8929  ltsosr  8974  recexsrlem  8983  mulgt0sr  8985  map2psrpr  8990  supsrlem  8991  axrrecex  9043  axpre-lttrn  9046  axpre-mulgt0  9048  axpre-sup  9049  axsup  9156  ltordlem  9557  ltord1  9558  wloglei  9564  squeeze0  9918  infm3  9972  nnsub  10043  nnunb  10222  peano5uzti  10364  uzindOLD  10369  fzind  10373  eluzadd  10519  eluzsub  10520  uzind4s  10541  uzind4s2  10542  zmax  10576  zbtwnre  10577  xmulasslem  10869  xrsupsslem  10890  xrinfmsslem  10891  xrub  10895  injresinj  11205  om2uzlti  11295  uzindi  11325  axdc4uz  11327  seqp1  11343  seqcl2  11346  seqfveq2  11350  seqshft2  11354  monoord  11358  seqsplit  11361  seqf1olem2  11368  seqf1o  11369  seqid2  11374  seqhomo  11375  seqof2  11386  expcl2lem  11398  facdiv  11583  facwordi  11585  faclbnd4lem2  11590  hashnn0n0nn  11669  hashf1lem2  11710  seqcoll  11717  brfi1uzind  11720  wrdind  11796  rlim2  12295  ello1mpt  12320  rlimclim1  12344  o1co  12385  o1compt  12386  rlimcn1  12387  rlimcn2  12389  climcn1  12390  climcn2  12391  subcn2  12393  o1of2  12411  caucvgrlem  12471  fsum2d  12560  fsumabs  12585  fsumtscopo  12586  fsumrlim  12595  fsumo1  12596  o1fsum  12597  fsumiun  12605  rpnnen2lem10  12828  sqr2irr  12853  dvdsle  12900  divalglem7  12924  divalglem8  12925  ndvdssub  12932  gcdcllem1  13016  algcvg  13072  algcvga  13075  algfx  13076  isprm2lem  13091  prmind2  13095  dvdsprime  13097  nprm  13098  dvdsprm  13104  coprm  13105  coprmdvds2  13108  isprm6  13114  exprmfct  13115  prmfac1  13123  eulerthlem2  13176  pcqmul  13232  pcqcl  13235  pc2dvds  13257  pcz  13259  prmpwdvds  13277  infpn2  13286  vdwlem12  13365  ramub2  13387  rami  13388  ramcl  13402  prmlem0  13433  mreintcl  13825  ismred2  13833  mrissmrcd  13870  mreexexlemd  13874  iscatd2  13911  moni  13967  yoniso  14387  isprs  14392  prslem  14393  drsdirfi  14400  ispos  14409  posi  14412  isposd  14417  lubfval  14440  lubid  14444  glbfval  14445  joinle  14455  meetle  14462  isclat  14543  clatlem  14544  clatl  14548  lubl  14552  lubun  14555  clatleglb  14558  pospropd  14566  poslubmo  14578  ipodrsima  14596  acsdrsel  14598  isacs4lem  14599  isacs5lem  14600  acsdrscl  14601  mreclat  14618  pslem  14643  spwval2  14661  spwmo  14663  dirtr  14686  isnsg2  14975  ghmf1  15039  orbsta  15095  sylow1lem1  15237  sylow2alem2  15257  sylow2a  15258  lsmmod  15312  lsmdisj2  15319  efgsrel  15371  efgredlemd  15381  efgredlem  15384  efgred  15385  gsumzaddlem  15531  dprdval  15566  dprddisj2  15602  ablfac1eulem  15635  pgpfac1lem1  15637  pgpfac1lem5  15642  pgpfac1  15643  pgpfaclem2  15645  pgpfac  15647  irredmul  15819  isdrngrd  15866  islbs3  16232  rrgval  16352  rrgeq0i  16354  isdomn  16359  domneq0  16362  mplsubglem  16503  mpllsslem  16504  mplcoe1  16533  mplcoe2  16535  prmirredlem  16778  znfld  16846  znrrg  16851  cygznlem3  16855  isphl  16864  ipeq0  16874  isphld  16890  phlpropd  16891  lsmcss  16924  uniopn  16975  fiinopn  16979  epttop  17078  clsndisj  17144  elcls3  17152  neiptoptop  17200  neiptopnei  17201  cnpval  17305  iscnp  17306  cnpimaex  17325  lmcvg  17331  cnprest  17358  cnprest2  17359  lmss  17367  lmff  17370  ist1  17390  t0sep  17393  hausnei  17397  isnrm2  17427  t1sep2  17438  isreg2  17446  iscmp  17456  cmpcov  17457  cmpsublem  17467  cmpsub  17468  tgcmp  17469  uncmp  17471  fiuncmp  17472  hauscmplem  17474  cmpfi  17476  cmpfii  17477  bwth  17478  dfcon2  17487  consuba  17488  connsub  17489  nconsubb  17491  1stcclb  17512  1stcfb  17513  2ndc1stc  17519  1stcrest  17521  1stcelcls  17529  restnlly  17550  lly1stc  17564  kgenval  17572  kgeni  17574  kgencn2  17594  ptcldmpt  17651  ptclsg  17652  dfac14lem  17654  dfac14  17655  txcnp  17657  ptcnp  17659  hausdiag  17682  txlm  17685  tx1stc  17687  xkococn  17697  cnmpt12  17704  cnmpt22  17711  kqt0lem  17773  isr0  17774  regr1lem2  17777  kqreglem1  17778  r0sep  17785  ptcmpfi  17850  elmptrab  17864  isfil  17884  filss  17890  isufil2  17945  cfinufil  17965  rnelfm  17990  fmfnfmlem2  17992  fmfnfmlem4  17994  flimopn  18012  flimrest  18020  flftg  18033  cnpflf  18038  txflf  18043  fclsopni  18052  fclsrest  18061  fclscf  18062  flimfnfcls  18065  fcfnei  18072  alexsublem  18080  alexsubb  18082  alexsubALTlem3  18085  alexsubALTlem4  18086  alexsubALT  18087  cnextcn  18103  cnextfres  18104  tgpt0  18153  divstgplem  18155  tsmsi  18168  tsmssubm  18177  tsmsres  18178  tsmsf1o  18179  tsmsxp  18189  ustssel  18240  ust0  18254  ustuqtop4  18279  ucnima  18316  ucncn  18320  iscusp  18334  cuspcvg  18336  imasdsf1olem  18408  blssps  18459  blss  18460  metss  18543  comet  18548  metcnp3  18575  metcnp2  18577  txmetcnp  18582  metuel2  18614  metucnOLD  18623  metucn  18624  nrmmetd  18627  nlmvscn  18728  nrginvrcn  18732  nmolb  18756  xrge0tsms  18870  divcn  18903  fsumcn  18905  elcncf2  18925  cncfi  18929  mulc1cncf  18940  cncfco  18942  cncfmet  18943  xrhmeo  18976  bndth  18988  nmoleub2lem2  19129  nmoleub3  19132  ipcn  19205  lmmbr  19216  caucfil  19241  pmltpc  19352  ovolfiniun  19402  ovolicc2lem3  19420  ovolicc2  19423  mblsplit  19433  finiunmbl  19443  volfiniun  19446  voliunlem3  19451  ioorinv  19473  ioorcl  19474  dyadmax  19495  dyadmbllem  19496  dyadmbl  19497  opnmbllem  19498  volcn  19503  vitalilem2  19506  vitalilem3  19507  vitali  19510  i1fd  19576  itg2seq  19637  itg2addlem  19653  itgfsum  19721  ellimc3  19771  dvbsss  19794  dvnres  19822  dvmptfsum  19864  dvferm1lem  19873  dvferm2lem  19875  rolle  19879  c1lip1  19886  lhop1lem  19902  lhop1  19903  dvfsumlem2  19916  dvfsumlem4  19918  dvfsumrlim  19920  dvfsum2  19923  ftc1a  19926  ftc1lem4  19928  ftc1lem6  19930  mpfind  19970  pf1ind  19980  mdegleb  19992  mdeglt  19993  deg1leb  20023  deg1lt  20025  ply1divex  20064  fta1glem2  20094  fta1g  20095  plyco0  20116  plyeq0lem  20134  coeeq2  20166  dgrle  20167  dgrcolem2  20197  dgrco  20198  plydivlem4  20218  plydivex  20219  fta1lem  20229  fta1  20230  vieta1lem2  20233  vieta1  20234  aalioulem2  20255  aalioulem4  20257  abelth  20362  cxpcn3  20637  rlimcnp  20809  xrlimcnp  20812  cxploglim  20821  scvxcvx  20829  jensen  20832  wilthlem2  20857  wilthlem3  20858  fta  20867  dvdsmulf1o  20984  perfectlem2  21019  dchrelbas3  21027  dchrelbas4  21032  dchrn0  21039  bcmono  21066  lgsdir2lem4  21115  lgsdchr  21137  lgseisenlem2  21139  lgsquad2lem2  21148  2sqlem6  21158  2sqlem8  21161  2sqlem10  21163  dchrisumlema  21187  dchrisumlem2  21189  dchrisumlem3  21190  wlkntrllem3  21566  1pthoncl  21597  2pthoncl  21608  fargshiftf1  21629  constr3trllem2  21643  eupatrl  21695  eupath2  21707  isass  21909  ismgm  21913  isexid2  21918  nvz  22163  nmobndseqi  22285  nmobndseqiOLD  22286  nmlno0  22301  blocnilem  22310  dipdir  22348  dipass  22351  siilem2  22358  ubthlem2  22378  ubth  22380  htth  22426  normpyth  22652  norm3lemt  22659  chlimi  22742  chcompl  22750  omlsii  22910  pjoml  22943  h1de2i  23060  elspansn2  23074  h1datom  23089  pjoml2  23118  pjoml3  23119  lecm  23124  chscllem2  23145  osum  23152  spansncv  23160  pjcjt2  23199  pjopyth  23227  eigre  23343  eigorth  23346  hhcno  23412  hhcnf  23413  cnopc  23421  cnfnc  23438  nmcexi  23534  nmcopexi  23535  nmcfnexi  23559  pjssge0i  23674  hstel2  23727  stj  23743  stri  23765  hstri  23773  stcltr1i  23782  mdbr  23802  mdi  23803  mdbr3  23805  mdbr4  23806  dmdbr  23807  dmdmd  23808  dmdi  23810  dmdbr3  23813  dmdbr4  23814  dmdbr5  23816  mdsl1i  23829  mdslmd1lem3  23835  mdslmd1lem4  23836  mdslmd1i  23837  csmdsymi  23842  cvmd  23844  atss  23854  atom1d  23861  chcv1  23863  hatomic  23868  atord  23896  atcvat2  23897  mddmdin0i  23939  rmoxfrdOLD  23984  rmoxfrd  23985  ifeqeqx  24006  ssiun2sf  24015  fmptcof2  24081  resspos  24192  toslub  24196  tosglb  24197  xrge0tsmsd  24228  isofld  24240  ofldadd  24243  ofldmul  24244  kerf1hrm  24267  xrge0iifiso  24326  esumcvg  24481  isrnsigaOLD  24500  sigaclcu  24505  sigaclci  24520  unelsiga  24522  measvun  24568  measiun  24577  sibfof  24659  sitgclg  24661  lgamgulmlem2  24819  subfacp1lem6  24876  erdszelem9  24890  kur14lem9  24905  sconpht  24921  cvmsss2  24966  cvmliftlem7  24983  cvmliftlem10  24986  ghomf1olem  25110  relexpsucr  25135  relexpsucl  25137  relexpcnv  25138  relexpdm  25140  relexprn  25141  relexpadd  25143  relexpindlem  25144  rtrclreclem.min  25152  iota5f  25187  dedekind  25192  prodfdiv  25229  fprod2d  25310  dfpo2  25383  fununiq  25399  setinds  25410  dfon2lem3  25417  dfon2lem4  25418  dfon2lem5  25419  dfon2lem6  25420  dfon2lem7  25421  dfon2lem8  25422  dfon2  25424  predbrg  25466  preddowncl  25476  tfisg  25484  wfisg  25489  frmin  25522  frinsg  25525  wfrlem9  25551  frrlem5e  25595  nocvxminlem  25650  axcgrtr  25859  btwnconn1lem11  26036  linethru  26092  rankelg  26114  rankeq1o  26117  heicant  26253  mblfinlem1  26255  mblfinlem2  26256  mblfinlem3  26257  voliunnfl  26262  volsupnfl  26263  mbfresfi  26265  itg2addnclem3  26272  itg2gt0cn  26274  ftc1cnnclem  26292  ftc1cnnc  26293  ftc1anclem7  26300  ftc1anc  26302  subtr  26331  subtr2  26332  trer  26333  nn0prpwlem  26339  nn0prpw  26340  comppfsc  26401  neibastop2lem  26403  filnetlem4  26424  f1opr  26440  sdclem2  26460  fdc  26463  fdc1  26464  neificl  26473  mettrifi  26477  sstotbnd2  26497  cntotbnd  26519  heibor1lem  26532  bfp  26547  iscringd  26623  ispridl  26658  pridl  26661  ismaxidl  26664  maxidlmax  26667  ispridlc  26694  pridlc  26695  dmnnzd  26699  ismrcd1  26766  ismrcd2  26767  ismrc  26769  isnacs3  26778  nacsfix  26780  mzpcompact2  26823  fphpd  26891  fphpdo  26892  monotuz  27018  monotoddzzfi  27019  monotoddzz  27020  oddcomabszz  27021  zindbi  27023  setindtrs  27110  dford3lem2  27112  ttac  27121  dnnumch1  27133  fnwe2lem2  27140  aomclem3  27145  aomclem6  27148  aomclem8  27150  dfac11  27151  dfac21  27155  islssfg2  27160  frlmup1  27241  lindfrn  27282  islindf4  27299  islindf5  27300  hbtlem5  27323  hbt  27325  flcidc  27370  symggen  27402  psgnunilem4  27411  mendlmod  27492  sdrgacs  27500  pm14.122b  27614  sbiota1  27625  fnchoice  27690  fmul01  27700  fmulcl  27701  fmuldfeqlem1  27702  fmuldfeq  27703  fmul01lt1lem1  27704  fmul01lt1lem2  27705  climmulf  27720  climexp  27721  climsuse  27724  climrecf  27725  climinff  27727  stoweidlem3  27742  stoweidlem4  27743  stoweidlem6  27745  stoweidlem8  27747  stoweidlem15  27754  stoweidlem16  27755  stoweidlem17  27756  stoweidlem19  27758  stoweidlem20  27759  stoweidlem22  27761  stoweidlem23  27762  stoweidlem26  27765  stoweidlem27  27766  stoweidlem30  27769  stoweidlem31  27770  stoweidlem32  27771  stoweidlem34  27773  stoweidlem35  27774  stoweidlem42  27781  stoweidlem43  27782  stoweidlem48  27787  stoweidlem50  27789  stoweidlem51  27790  stoweidlem57  27796  stoweidlem59  27798  stoweidlem62  27801  wallispilem3  27806  sbcfun  27977  swrdccatin1  28239  swrdccat3blem  28252  usgra2pthspth  28343  usgra2wlkspthlem1  28344  usgra2wlkspthlem2  28345  usgra2pthlem1  28348  frgra3vlem1  28464  3vfriswmgralem  28468  3vfriswmgra  28469  frgrawopreglem4  28510  frg2wot1  28520  frg2woteqm  28522  usg2spot2nb  28528  imbi12  28677  sbcssOLD  28701  bnj1385  29278  bnj110  29303  bnj222  29328  bnj229  29329  bnj590  29355  bnj865  29368  bnj849  29370  bnj981  29395  bnj1014  29405  bnj1015  29406  bnj1112  29426  bnj1118  29427  bnj1123  29429  bnj1128  29433  bnj1125  29435  bnj1148  29439  bnj1154  29442  bnj1326  29469  bnj1384  29475  bnj1489  29499  bnj1497  29503  drnf1NEW7  29569  drnf2wAUX7  29572  drnf2w2AUX7  29575  drnf2w3AUX7  29578  equveliNEW7  29602  ax11v2NEW7  29604  drnf2OLD7  29790  lubunNEW  29845  lshpdisj  29859  lsmsatcv  29882  lsat0cv  29905  lcvexchlem4  29909  lcvexchlem5  29910  l1cvpat  29926  isopos  30052  oposlem  30055  isoml  30110  omllaw  30115  isatl  30171  atlex  30188  iscvlat  30195  cvlexch1  30200  glbconN  30248  hlsuprexch  30252  ps-1  30348  3atlem5  30358  psubspi  30618  llnexchb2  30740  elpcliN  30764  pclfinclN  30821  ldilval  30984  ltrnfset  30988  ltrnset  30989  ltrnu  30992  trlfset  31031  trlset  31032  trlval2  31034  cdleme25cv  31229  cdleme31so  31250  cdleme31fv  31261  cdlemefrs29bpre0  31267  cdleme32fva  31308  cdleme40v  31340  trlord  31440  cdlemkid3N  31804  cdlemkid4  31805  dihffval  32102  dihfval  32103  dihval  32104  lpolconN  32359  mapdordlem2  32509  hdmapfval  32702  hdmapval  32703  hdmapval2  32707
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 179
  Copyright terms: Public domain W3C validator