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  4311  trss  4313  zfpow  4380  rext  4414  opth  4437  copsexg  4444  poeq1  4508  pocl  4512  swopolem  4514  swopo  4515  isso2i  4537  fri  4546  ordelord  4605  reusv2lem4  4729  reusv3i  4732  tfis  4836  tfisi  4840  tfindsg  4842  tfindsg2  4843  tfindes  4844  dfom2  4849  limomss  4852  nnlim  4860  findsg  4874  findes  4877  vtoclr  4924  poinxp  4943  posn  4948  ssrel  4966  ssrel2  4968  ssrelrel  4978  relop  5025  issref  5249  iota5  5440  funopg  5487  brprcneu  5723  tz6.12f  5751  funbrfv  5767  ssimaexg  5791  fvmptf  5823  fvelrn  5868  fprg  5917  f1veqaeq  6007  dff13f  6008  soisores  6049  soisoi  6050  isofrlem  6062  isopolem  6067  f1oweALT  6076  weniso  6077  oprabid  6107  ovmpt2s  6199  ov2gf  6200  ov3  6212  caovcan  6253  caovordig  6254  caofrss  6339  caoftrn  6341  dfoprab4f  6407  f1o2ndf1  6456  frxp  6458  poxp  6460  riota5f  6576  riotasv2d  6596  riotasv2dOLD  6597  onfununi  6605  smoel  6624  smogt  6631  tfrlem1  6638  tz7.48lem  6700  tz7.49  6704  oawordeu  6800  omordi  6811  oeordi  6832  nnmordi  6876  omabs  6892  nneob  6897  omsmolem  6898  qsel  6985  eroveu  7001  ecopovtrn  7009  th3qlem2  7013  ixpsnf1o  7104  fundmeng  7183  sbth  7229  limensuc  7286  nneneq  7292  php  7293  php2  7294  unxpdom  7318  pssnn  7329  findcard  7349  findcard2  7350  findcard3  7352  ac6sfi  7353  frfi  7354  domunfican  7381  fiint  7385  iunfi  7396  finsschain  7415  dffi3  7438  marypha1lem  7440  marypha1  7441  supeq3  7456  supeq123d  7457  supmo  7459  suplub  7467  supisolem  7477  ordiso2  7486  ordtypelem7  7495  wemaplem1  7517  wemaplem2  7518  zfregcl  7564  inf0  7578  inf3lem1  7585  zfinf  7596  axinf2  7597  dfom3  7604  elom3  7605  cantnfval2  7626  cantnfle  7628  cantnflt  7629  cantnfp1lem3  7638  oemapvali  7642  cantnflem1c  7645  cantnflem1  7647  cantnf  7651  wemapwe  7656  cnfcom  7659  setind  7675  r1sdom  7702  r1ordg  7706  rankonidlem  7756  rankunb  7778  bnd2  7819  infxpenlem  7897  infxpenc2  7905  dfac8alem  7912  dfac8clem  7915  indcardi  7924  alephordi  7957  alephinit  7978  alephfp  7991  aceq3lem  8003  dfac5lem4  8009  dfac5  8011  dfac2  8013  dfac9  8018  dfac12lem2  8026  dfac12lem3  8027  kmlem1  8032  kmlem4  8035  kmlem10  8041  kmlem12  8043  kmlem13  8044  pwsdompw  8086  ackbij1lem16  8117  cfslb2n  8150  cfsmolem  8152  sornom  8159  fin2i  8177  infpssrlem4  8188  isfin2-2  8201  isfin3ds  8211  fin23lem17  8220  fin23lem32  8226  fin23lem34  8228  fin23lem35  8229  fin23lem39  8232  fin23lem41  8234  isf32lem2  8236  isf33lem  8248  isf34lem4  8259  isf34lem6  8262  fin1a2lem10  8291  axcc2lem  8318  axcc3  8320  axcc4dom  8323  dominf  8327  axdc2lem  8330  axdc3lem2  8333  ac6sg  8370  zorn2lem7  8384  zornn0g  8387  ttukeylem5  8395  ttukeylem6  8396  axdclem  8401  fodomg  8405  dominfac  8450  axrepndlem1  8469  axrepndlem2  8470  axunndlem1  8472  axunnd  8473  axpowndlem2  8475  axpowndlem3  8476  axpowndlem4  8477  axregndlem2  8480  axregnd  8481  axinfndlem1  8482  axinfnd  8483  axacndlem4  8487  axacndlem5  8488  axacnd  8489  zfcndpow  8493  zfcndinf  8495  fpwwe2lem5  8511  fpwwe2lem8  8514  fpwwe2lem12  8518  pwfseqlem4a  8538  pwfseqlem4  8539  pwfseqlem5  8540  pwfseq  8541  wunfi  8598  wunex2  8615  inar1  8652  rankcf  8654  tskord  8657  grudomon  8694  grur1a  8696  axgroth6  8705  axgroth3  8708  axgroth4  8709  eltskm  8720  indpi  8786  pinq  8806  nqereu  8808  prcdnq  8872  prnmax  8874  ltsopr  8911  prlem936  8926  ltsosr  8971  recexsrlem  8980  mulgt0sr  8982  map2psrpr  8987  supsrlem  8988  axrrecex  9040  axpre-lttrn  9043  axpre-mulgt0  9045  axpre-sup  9046  axsup  9153  ltordlem  9554  ltord1  9555  wloglei  9561  squeeze0  9915  infm3  9969  nnsub  10040  nnunb  10219  peano5uzti  10361  uzindOLD  10366  fzind  10370  eluzadd  10516  eluzsub  10517  uzind4s  10538  uzind4s2  10539  zmax  10573  zbtwnre  10574  xmulasslem  10866  xrsupsslem  10887  xrinfmsslem  10888  xrub  10892  injresinj  11202  om2uzlti  11292  uzindi  11322  axdc4uz  11324  seqp1  11340  seqcl2  11343  seqfveq2  11347  seqshft2  11351  monoord  11355  seqsplit  11358  seqf1olem2  11365  seqf1o  11366  seqid2  11371  seqhomo  11372  seqof2  11383  expcl2lem  11395  facdiv  11580  facwordi  11582  faclbnd4lem2  11587  hashnn0n0nn  11666  hashf1lem2  11707  seqcoll  11714  brfi1uzind  11717  wrdind  11793  rlim2  12292  ello1mpt  12317  rlimclim1  12341  o1co  12382  o1compt  12383  rlimcn1  12384  rlimcn2  12386  climcn1  12387  climcn2  12388  subcn2  12390  o1of2  12408  caucvgrlem  12468  fsum2d  12557  fsumabs  12582  fsumtscopo  12583  fsumrlim  12592  fsumo1  12593  o1fsum  12594  fsumiun  12602  rpnnen2lem10  12825  sqr2irr  12850  dvdsle  12897  divalglem7  12921  divalglem8  12922  ndvdssub  12929  gcdcllem1  13013  algcvg  13069  algcvga  13072  algfx  13073  isprm2lem  13088  prmind2  13092  dvdsprime  13094  nprm  13095  dvdsprm  13101  coprm  13102  coprmdvds2  13105  isprm6  13111  exprmfct  13112  prmfac1  13120  eulerthlem2  13173  pcqmul  13229  pcqcl  13232  pc2dvds  13254  pcz  13256  prmpwdvds  13274  infpn2  13283  vdwlem12  13362  ramub2  13384  rami  13385  ramcl  13399  prmlem0  13430  mreintcl  13822  ismred2  13830  mrissmrcd  13867  mreexexlemd  13871  iscatd2  13908  moni  13964  yoniso  14384  isprs  14389  prslem  14390  drsdirfi  14397  ispos  14406  posi  14409  isposd  14414  lubfval  14437  lubid  14441  glbfval  14442  joinle  14452  meetle  14459  isclat  14540  clatlem  14541  clatl  14545  lubl  14549  lubun  14552  clatleglb  14555  pospropd  14563  poslubmo  14575  ipodrsima  14593  acsdrsel  14595  isacs4lem  14596  isacs5lem  14597  acsdrscl  14598  mreclat  14615  pslem  14640  spwval2  14658  spwmo  14660  dirtr  14683  isnsg2  14972  ghmf1  15036  orbsta  15092  sylow1lem1  15234  sylow2alem2  15254  sylow2a  15255  lsmmod  15309  lsmdisj2  15316  efgsrel  15368  efgredlemd  15378  efgredlem  15381  efgred  15382  gsumzaddlem  15528  dprdval  15563  dprddisj2  15599  ablfac1eulem  15632  pgpfac1lem1  15634  pgpfac1lem5  15639  pgpfac1  15640  pgpfaclem2  15642  pgpfac  15644  irredmul  15816  isdrngrd  15863  islbs3  16229  rrgval  16349  rrgeq0i  16351  isdomn  16356  domneq0  16359  mplsubglem  16500  mpllsslem  16501  mplcoe1  16530  mplcoe2  16532  prmirredlem  16775  znfld  16843  znrrg  16848  cygznlem3  16852  isphl  16861  ipeq0  16871  isphld  16887  phlpropd  16888  lsmcss  16921  uniopn  16972  fiinopn  16976  epttop  17075  clsndisj  17141  elcls3  17149  neiptoptop  17197  neiptopnei  17198  cnpval  17302  iscnp  17303  cnpimaex  17322  lmcvg  17328  cnprest  17355  cnprest2  17356  lmss  17364  lmff  17367  ist1  17387  t0sep  17390  hausnei  17394  isnrm2  17424  t1sep2  17435  isreg2  17443  iscmp  17453  cmpcov  17454  cmpsublem  17464  cmpsub  17465  tgcmp  17466  uncmp  17468  fiuncmp  17469  hauscmplem  17471  cmpfi  17473  cmpfii  17474  bwth  17475  dfcon2  17484  consuba  17485  connsub  17486  nconsubb  17488  1stcclb  17509  1stcfb  17510  2ndc1stc  17516  1stcrest  17518  1stcelcls  17526  restnlly  17547  lly1stc  17561  kgenval  17569  kgeni  17571  kgencn2  17591  ptcldmpt  17648  ptclsg  17649  dfac14lem  17651  dfac14  17652  txcnp  17654  ptcnp  17656  hausdiag  17679  txlm  17682  tx1stc  17684  xkococn  17694  cnmpt12  17701  cnmpt22  17708  kqt0lem  17770  isr0  17771  regr1lem2  17774  kqreglem1  17775  r0sep  17782  ptcmpfi  17847  elmptrab  17861  isfil  17881  filss  17887  isufil2  17942  cfinufil  17962  rnelfm  17987  fmfnfmlem2  17989  fmfnfmlem4  17991  flimopn  18009  flimrest  18017  flftg  18030  cnpflf  18035  txflf  18040  fclsopni  18049  fclsrest  18058  fclscf  18059  flimfnfcls  18062  fcfnei  18069  alexsublem  18077  alexsubb  18079  alexsubALTlem3  18082  alexsubALTlem4  18083  alexsubALT  18084  cnextcn  18100  cnextfres  18101  tgpt0  18150  divstgplem  18152  tsmsi  18165  tsmssubm  18174  tsmsres  18175  tsmsf1o  18176  tsmsxp  18186  ustssel  18237  ust0  18251  ustuqtop4  18276  ucnima  18313  ucncn  18317  iscusp  18331  cuspcvg  18333  imasdsf1olem  18405  blssps  18456  blss  18457  metss  18540  comet  18545  metcnp3  18572  metcnp2  18574  txmetcnp  18579  metuel2  18611  metucnOLD  18620  metucn  18621  nrmmetd  18624  nlmvscn  18725  nrginvrcn  18729  nmolb  18753  xrge0tsms  18867  divcn  18900  fsumcn  18902  elcncf2  18922  cncfi  18926  mulc1cncf  18937  cncfco  18939  cncfmet  18940  xrhmeo  18973  bndth  18985  nmoleub2lem2  19126  nmoleub3  19129  ipcn  19202  lmmbr  19213  caucfil  19238  pmltpc  19349  ovolfiniun  19399  ovolicc2lem3  19417  ovolicc2  19420  mblsplit  19430  finiunmbl  19440  volfiniun  19443  voliunlem3  19448  ioorinv  19470  ioorcl  19471  dyadmax  19492  dyadmbllem  19493  dyadmbl  19494  opnmbllem  19495  volcn  19500  vitalilem2  19503  vitalilem3  19504  vitali  19507  i1fd  19575  itg2seq  19636  itg2addlem  19652  itgfsum  19720  ellimc3  19768  dvbsss  19791  dvnres  19819  dvmptfsum  19861  dvferm1lem  19870  dvferm2lem  19872  rolle  19876  c1lip1  19883  lhop1lem  19899  lhop1  19900  dvfsumlem2  19913  dvfsumlem4  19915  dvfsumrlim  19917  dvfsum2  19920  ftc1a  19923  ftc1lem4  19925  ftc1lem6  19927  mpfind  19967  pf1ind  19977  mdegleb  19989  mdeglt  19990  deg1leb  20020  deg1lt  20022  ply1divex  20061  fta1glem2  20091  fta1g  20092  plyco0  20113  plyeq0lem  20131  coeeq2  20163  dgrle  20164  dgrcolem2  20194  dgrco  20195  plydivlem4  20215  plydivex  20216  fta1lem  20226  fta1  20227  vieta1lem2  20230  vieta1  20231  aalioulem2  20252  aalioulem4  20254  abelth  20359  cxpcn3  20634  rlimcnp  20806  xrlimcnp  20809  cxploglim  20818  scvxcvx  20826  jensen  20829  wilthlem2  20854  wilthlem3  20855  fta  20864  dvdsmulf1o  20981  perfectlem2  21016  dchrelbas3  21024  dchrelbas4  21029  dchrn0  21036  bcmono  21063  lgsdir2lem4  21112  lgsdchr  21134  lgseisenlem2  21136  lgsquad2lem2  21145  2sqlem6  21155  2sqlem8  21158  2sqlem10  21160  dchrisumlema  21184  dchrisumlem2  21186  dchrisumlem3  21187  wlkntrllem3  21563  1pthoncl  21594  2pthoncl  21605  fargshiftf1  21626  constr3trllem2  21640  eupatrl  21692  eupath2  21704  isass  21906  ismgm  21910  isexid2  21915  nvz  22160  nmobndseqi  22282  nmobndseqiOLD  22283  nmlno0  22298  blocnilem  22307  dipdir  22345  dipass  22348  siilem2  22355  ubthlem2  22375  ubth  22377  htth  22423  normpyth  22649  norm3lemt  22656  chlimi  22739  chcompl  22747  omlsii  22907  pjoml  22940  h1de2i  23057  elspansn2  23071  h1datom  23086  pjoml2  23115  pjoml3  23116  lecm  23121  chscllem2  23142  osum  23149  spansncv  23157  pjcjt2  23196  pjopyth  23224  eigre  23340  eigorth  23343  hhcno  23409  hhcnf  23410  cnopc  23418  cnfnc  23435  nmcexi  23531  nmcopexi  23532  nmcfnexi  23556  pjssge0i  23671  hstel2  23724  stj  23740  stri  23762  hstri  23770  stcltr1i  23779  mdbr  23799  mdi  23800  mdbr3  23802  mdbr4  23803  dmdbr  23804  dmdmd  23805  dmdi  23807  dmdbr3  23810  dmdbr4  23811  dmdbr5  23813  mdsl1i  23826  mdslmd1lem3  23832  mdslmd1lem4  23833  mdslmd1i  23834  csmdsymi  23839  cvmd  23841  atss  23851  atom1d  23858  chcv1  23860  hatomic  23865  atord  23893  atcvat2  23894  mddmdin0i  23936  rmoxfrdOLD  23981  rmoxfrd  23982  ifeqeqx  24003  ssiun2sf  24012  fmptcof2  24078  resspos  24189  toslub  24193  tosglb  24194  xrge0tsmsd  24225  isofld  24237  ofldadd  24240  ofldmul  24241  kerf1hrm  24264  xrge0iifiso  24323  esumcvg  24478  isrnsigaOLD  24497  sigaclcu  24502  sigaclci  24517  unelsiga  24519  measvun  24565  measiun  24574  sibfof  24656  sitgclg  24658  lgamgulmlem2  24816  subfacp1lem6  24873  erdszelem9  24887  kur14lem9  24902  sconpht  24918  cvmsss2  24963  cvmliftlem7  24980  cvmliftlem10  24983  ghomf1olem  25107  relexpsucr  25132  relexpsucl  25134  relexpcnv  25135  relexpdm  25137  relexprn  25138  relexpadd  25140  relexpindlem  25141  rtrclreclem.min  25149  iota5f  25184  dedekind  25189  prodfdiv  25226  fprod2d  25307  dfpo2  25380  fununiq  25396  setinds  25407  dfon2lem3  25414  dfon2lem4  25415  dfon2lem5  25416  dfon2lem6  25417  dfon2lem7  25418  dfon2lem8  25419  dfon2  25421  predbrg  25463  preddowncl  25473  tfisg  25481  wfisg  25486  frmin  25519  frinsg  25522  wfrlem9  25548  frrlem5e  25592  nocvxminlem  25647  axcgrtr  25856  btwnconn1lem11  26033  linethru  26089  rankelg  26111  rankeq1o  26114  mblfinlem1  26245  mblfinlem2  26246  mblfinlem3  26247  voliunnfl  26252  volsupnfl  26253  mbfresfi  26255  itg2addnclem3  26260  itg2gt0cn  26262  ftc1cnnclem  26280  ftc1cnnc  26281  ftc1anclem7  26288  ftc1anc  26290  subtr  26319  subtr2  26320  trer  26321  nn0prpwlem  26327  nn0prpw  26328  comppfsc  26389  neibastop2lem  26391  filnetlem4  26412  f1opr  26428  sdclem2  26448  fdc  26451  fdc1  26452  neificl  26461  mettrifi  26465  sstotbnd2  26485  cntotbnd  26507  heibor1lem  26520  bfp  26535  iscringd  26611  ispridl  26646  pridl  26649  ismaxidl  26652  maxidlmax  26655  ispridlc  26682  pridlc  26683  dmnnzd  26687  ismrcd1  26754  ismrcd2  26755  ismrc  26757  isnacs3  26766  nacsfix  26768  mzpcompact2  26811  fphpd  26879  fphpdo  26880  monotuz  27006  monotoddzzfi  27007  monotoddzz  27008  oddcomabszz  27009  zindbi  27011  setindtrs  27098  dford3lem2  27100  ttac  27109  dnnumch1  27121  fnwe2lem2  27128  aomclem3  27133  aomclem6  27136  aomclem8  27138  dfac11  27139  dfac21  27143  islssfg2  27148  frlmup1  27229  lindfrn  27270  islindf4  27287  islindf5  27288  hbtlem5  27311  hbt  27313  flcidc  27358  symggen  27390  psgnunilem4  27399  mendlmod  27480  sdrgacs  27488  pm14.122b  27602  sbiota1  27613  fnchoice  27678  fmul01  27688  fmulcl  27689  fmuldfeqlem1  27690  fmuldfeq  27691  fmul01lt1lem1  27692  fmul01lt1lem2  27693  climmulf  27708  climexp  27709  climsuse  27712  climrecf  27713  climinff  27715  stoweidlem3  27730  stoweidlem4  27731  stoweidlem6  27733  stoweidlem8  27735  stoweidlem15  27742  stoweidlem16  27743  stoweidlem17  27744  stoweidlem19  27746  stoweidlem20  27747  stoweidlem22  27749  stoweidlem23  27750  stoweidlem26  27753  stoweidlem27  27754  stoweidlem30  27757  stoweidlem31  27758  stoweidlem32  27759  stoweidlem34  27761  stoweidlem35  27762  stoweidlem42  27769  stoweidlem43  27770  stoweidlem48  27775  stoweidlem50  27777  stoweidlem51  27778  stoweidlem57  27784  stoweidlem59  27786  stoweidlem62  27789  wallispilem3  27794  sbcfun  27965  swrdccatin1  28227  swrdccat3blem  28240  usgra2pthspth  28331  usgra2wlkspthlem1  28332  usgra2wlkspthlem2  28333  usgra2pthlem1  28336  frgra3vlem1  28452  3vfriswmgralem  28456  3vfriswmgra  28457  frgrawopreglem4  28498  frg2wot1  28508  frg2woteqm  28510  usg2spot2nb  28516  imbi12  28665  sbcssOLD  28689  bnj1385  29266  bnj110  29291  bnj222  29316  bnj229  29317  bnj590  29343  bnj865  29356  bnj849  29358  bnj981  29383  bnj1014  29393  bnj1015  29394  bnj1112  29414  bnj1118  29415  bnj1123  29417  bnj1128  29421  bnj1125  29423  bnj1148  29427  bnj1154  29430  bnj1326  29457  bnj1384  29463  bnj1489  29487  bnj1497  29491  drnf1NEW7  29557  drnf2wAUX7  29560  drnf2w2AUX7  29563  drnf2w3AUX7  29566  equveliNEW7  29590  ax11v2NEW7  29592  drnf2OLD7  29778  lubunNEW  29833  lshpdisj  29847  lsmsatcv  29870  lsat0cv  29893  lcvexchlem4  29897  lcvexchlem5  29898  l1cvpat  29914  isopos  30040  oposlem  30043  isoml  30098  omllaw  30103  isatl  30159  atlex  30176  iscvlat  30183  cvlexch1  30188  glbconN  30236  hlsuprexch  30240  ps-1  30336  3atlem5  30346  psubspi  30606  llnexchb2  30728  elpcliN  30752  pclfinclN  30809  ldilval  30972  ltrnfset  30976  ltrnset  30977  ltrnu  30980  trlfset  31019  trlset  31020  trlval2  31022  cdleme25cv  31217  cdleme31so  31238  cdleme31fv  31249  cdlemefrs29bpre0  31255  cdleme32fva  31296  cdleme40v  31328  trlord  31428  cdlemkid3N  31792  cdlemkid4  31793  dihffval  32090  dihfval  32091  dihval  32092  lpolconN  32347  mapdordlem2  32497  hdmapfval  32690  hdmapval  32691  hdmapval2  32695
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 179
  Copyright terms: Public domain W3C validator