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

Theorem imbi12d 311
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 308 . 2  |-  ( ph  ->  ( ( ps  ->  th )  <->  ( ch  ->  th ) ) )
3 imbi12d.2 . . 3  |-  ( ph  ->  ( th  <->  ta )
)
43imbi2d 307 . 2  |-  ( ph  ->  ( ( ch  ->  th )  <->  ( ch  ->  ta ) ) )
52, 4bitrd 244 1  |-  ( ph  ->  ( ( ps  ->  th )  <->  ( ch  ->  ta ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176
This theorem is referenced by:  nfbidf  1754  drnf1  1909  drnf2  1910  equveli  1928  ax11v2  1932  ax10-16  2129  ax11eq  2132  ax11el  2133  ax11inda  2139  ax11v2-o  2140  mobid  2177  2mo  2221  2eu6  2228  axext3  2266  ralcom2  2704  cbvralf  2758  cbvraldva2  2768  vtoclgaf  2848  vtocl2gaf  2850  vtocl3gaf  2852  rspct  2877  rspc  2878  ceqex  2898  ralab2  2930  mob2  2945  mob  2947  morex  2949  reu7  2960  reu8  2961  cdeqim  2984  sbcimg  3032  csbhypf  3116  cbvralcsf  3143  dfss2f  3171  sbcss  3564  sneqrg  3782  elintab  3873  intss1  3877  intmin  3882  dfiin2g  3936  trel  4120  trss  4122  zfpow  4189  rext  4222  opth  4245  copsexg  4252  poeq1  4317  pocl  4321  swopolem  4323  swopo  4324  isso2i  4346  fri  4355  ordelord  4414  reusv2lem4  4538  reusv3i  4541  tfis  4645  tfisi  4649  tfindsg  4651  tfindsg2  4652  tfindes  4653  dfom2  4658  limomss  4661  nnlim  4669  findsg  4683  findes  4686  vtoclr  4733  poinxp  4753  posn  4758  ssrel  4776  ssrelrel  4787  relop  4834  issref  5056  iota5  5239  funopg  5286  brprcneu  5518  tz6.12f  5546  funbrfv  5561  ssimaexg  5585  fvmptf  5616  fvelrn  5661  dff13f  5784  f1fveq  5786  soisores  5824  soisoi  5825  isofrlem  5837  isopolem  5842  f1oweALT  5851  weniso  5852  oprabid  5882  ovmpt2s  5971  ov2gf  5972  ov3  5984  caovcan  6024  caovordig  6025  caofrss  6110  caoftrn  6112  dfoprab4f  6178  frxp  6225  poxp  6227  riota5f  6329  riotasv2d  6349  riotasv2dOLD  6350  onfununi  6358  smoel  6377  smogt  6384  tfrlem1  6391  tz7.48lem  6453  tz7.49  6457  oawordeu  6553  omordi  6564  oeordi  6585  nnmordi  6629  omabs  6645  nneob  6650  omsmolem  6651  qsel  6738  eroveu  6753  ecopovtrn  6761  th3qlem2  6765  ixpsnf1o  6856  fundmeng  6935  sbth  6981  limensuc  7038  nneneq  7044  php  7045  php2  7046  unxpdom  7070  pssnn  7081  findcard  7097  findcard2  7098  findcard3  7100  ac6sfi  7101  frfi  7102  domunfican  7129  fiint  7133  iunfi  7144  finsschain  7162  dffi3  7184  marypha1lem  7186  marypha1  7187  supmo  7203  suplub  7211  supisolem  7221  ordiso2  7230  ordtypelem7  7239  wemaplem1  7261  wemaplem2  7262  zfregcl  7308  inf0  7322  inf3lem1  7329  zfinf  7340  axinf2  7341  dfom3  7348  elom3  7349  cantnfval2  7370  cantnfle  7372  cantnflt  7373  cantnfp1lem3  7382  oemapvali  7386  cantnflem1c  7389  cantnflem1  7391  cantnf  7395  wemapwe  7400  cnfcom  7403  setind  7419  r1sdom  7446  r1ordg  7450  rankonidlem  7500  rankunb  7522  bnd2  7563  infxpenlem  7641  infxpenc2  7649  dfac8alem  7656  dfac8clem  7659  indcardi  7668  alephordi  7701  alephinit  7722  alephfp  7735  aceq3lem  7747  dfac5lem4  7753  dfac5  7755  dfac2  7757  dfac9  7762  dfac12lem2  7770  dfac12lem3  7771  kmlem1  7776  kmlem4  7779  kmlem10  7785  kmlem12  7787  kmlem13  7788  pwsdompw  7830  ackbij1lem16  7861  cfslb2n  7894  cfsmolem  7896  sornom  7903  fin2i  7921  infpssrlem4  7932  isfin2-2  7945  isfin3ds  7955  fin23lem17  7964  fin23lem32  7970  fin23lem34  7972  fin23lem35  7973  fin23lem39  7976  fin23lem41  7978  isf32lem2  7980  isf33lem  7992  isf34lem4  8003  isf34lem6  8006  fin1a2lem10  8035  axcc2lem  8062  axcc3  8064  axcc4dom  8067  dominf  8071  axdc2lem  8074  axdc3lem2  8077  ac6sg  8115  zorn2lem7  8129  zornn0g  8132  ttukeylem5  8140  ttukeylem6  8141  axdclem  8146  fodomg  8150  dominfac  8195  axrepndlem1  8214  axrepndlem2  8215  axunndlem1  8217  axunnd  8218  axpowndlem2  8220  axpowndlem3  8221  axpowndlem4  8222  axregndlem2  8225  axregnd  8226  axinfndlem1  8227  axinfnd  8228  axacndlem4  8232  axacndlem5  8233  axacnd  8234  zfcndpow  8238  zfcndinf  8240  fpwwe2lem5  8256  fpwwe2lem8  8259  fpwwe2lem12  8263  pwfseqlem4a  8283  pwfseqlem4  8284  pwfseqlem5  8285  pwfseq  8286  wunfi  8343  wunex2  8360  inar1  8397  rankcf  8399  tskord  8402  grudomon  8439  grur1a  8441  axgroth6  8450  axgroth3  8453  axgroth4  8454  eltskm  8465  indpi  8531  pinq  8551  nqereu  8553  prcdnq  8617  prnmax  8619  ltsopr  8656  prlem936  8671  ltsosr  8716  recexsrlem  8725  mulgt0sr  8727  map2psrpr  8732  supsrlem  8733  axrrecex  8785  axpre-lttrn  8788  axpre-mulgt0  8790  axpre-sup  8791  axsup  8898  ltordlem  9298  ltord1  9299  wloglei  9305  squeeze0  9659  infm3  9713  nnsub  9784  nnunb  9961  peano5uzti  10101  uzindOLD  10106  fzind  10110  eluzadd  10256  eluzsub  10257  uzind4s  10278  uzind4s2  10279  zmax  10313  zbtwnre  10314  xmulasslem  10605  xrsupsslem  10625  xrinfmsslem  10626  xrub  10630  om2uzlti  11013  uzindi  11043  axdc4uz  11045  seqp1  11061  seqcl2  11064  seqfveq2  11068  seqshft2  11072  monoord  11076  seqsplit  11079  seqf1olem2  11086  seqf1o  11087  seqid2  11092  seqhomo  11093  expcl2lem  11115  facdiv  11300  facwordi  11302  faclbnd4lem2  11307  hashf1lem2  11394  seqcoll  11401  wrdind  11477  rlim2  11970  ello1mpt  11995  rlimclim1  12019  o1co  12060  o1compt  12061  rlimcn1  12062  rlimcn2  12064  climcn1  12065  climcn2  12066  subcn2  12068  o1of2  12086  caucvgrlem  12145  fsum2d  12234  fsumabs  12259  fsumtscopo  12260  fsumrlim  12269  fsumo1  12270  o1fsum  12271  fsumiun  12279  rpnnen2lem10  12502  sqr2irr  12527  dvdsle  12574  divalglem7  12598  divalglem8  12599  ndvdssub  12606  gcdcllem1  12690  algcvg  12746  algcvga  12749  algfx  12750  isprm2lem  12765  prmind2  12769  dvdsprime  12771  nprm  12772  dvdsprm  12778  coprm  12779  coprmdvds2  12782  isprm6  12788  exprmfct  12789  prmfac1  12797  eulerthlem2  12850  pcqmul  12906  pcqcl  12909  pc2dvds  12931  pcz  12933  prmpwdvds  12951  infpn2  12960  vdwlem12  13039  ramub2  13061  rami  13062  ramcl  13076  prmlem0  13107  mreintcl  13497  ismred2  13505  mrissmrcd  13542  mreexexlemd  13546  iscatd2  13583  moni  13639  yoniso  14059  isprs  14064  prslem  14065  drsdirfi  14072  ispos  14081  posi  14084  isposd  14089  lubfval  14112  lubid  14116  glbfval  14117  joinle  14127  meetle  14134  isclat  14215  clatlem  14216  clatl  14220  lubl  14224  lubun  14227  clatleglb  14230  pospropd  14238  poslubmo  14250  ipodrsima  14268  acsdrsel  14270  isacs4lem  14271  isacs5lem  14272  acsdrscl  14273  mreclat  14290  pslem  14315  spwval2  14333  spwmo  14335  dirtr  14358  isnsg2  14647  ghmf1  14711  orbsta  14767  sylow1lem1  14909  sylow2alem2  14929  sylow2a  14930  lsmmod  14984  lsmdisj2  14991  efgsrel  15043  efgredlemd  15053  efgredlem  15056  efgred  15057  gsumzaddlem  15203  dprdval  15238  dprddisj2  15274  ablfac1eulem  15307  pgpfac1lem1  15309  pgpfac1lem5  15314  pgpfac1  15315  pgpfaclem2  15317  pgpfac  15319  irredmul  15491  isdrngrd  15538  islbs3  15908  rrgval  16028  rrgeq0i  16030  isdomn  16035  domneq0  16038  mplsubglem  16179  mpllsslem  16180  mplcoe1  16209  mplcoe2  16211  prmirredlem  16446  znfld  16514  znrrg  16519  cygznlem3  16523  isphl  16532  ipeq0  16542  isphld  16558  phlpropd  16559  lsmcss  16592  uniopn  16643  fiinopn  16647  epttop  16746  clsndisj  16812  elcls3  16820  cnpval  16966  iscnp  16967  cnpimaex  16986  lmcvg  16992  cnprest  17017  cnprest2  17018  lmss  17026  lmff  17029  ist1  17049  t0sep  17052  hausnei  17056  isnrm2  17086  t1sep2  17097  isreg2  17105  iscmp  17115  cmpcov  17116  cmpsublem  17126  cmpsub  17127  tgcmp  17128  uncmp  17130  fiuncmp  17131  hauscmplem  17133  cmpfi  17135  cmpfii  17136  dfcon2  17145  consuba  17146  connsub  17147  nconsubb  17149  1stcclb  17170  1stcfb  17171  2ndc1stc  17177  1stcrest  17179  1stcelcls  17187  restnlly  17208  lly1stc  17222  kgenval  17230  kgeni  17232  kgencn2  17252  ptcldmpt  17308  ptclsg  17309  dfac14lem  17311  dfac14  17312  txcnp  17314  ptcnp  17316  hausdiag  17339  txlm  17342  tx1stc  17344  xkococn  17354  cnmpt12  17361  cnmpt22  17368  kqt0lem  17427  isr0  17428  regr1lem2  17431  kqreglem1  17432  r0sep  17439  ptcmpfi  17504  elmptrab  17522  isfil  17542  filss  17548  isufil2  17603  cfinufil  17623  rnelfm  17648  fmfnfmlem2  17650  fmfnfmlem4  17652  flimopn  17670  flimrest  17678  flftg  17691  cnpflf  17696  txflf  17701  fclsopni  17710  fclsrest  17719  fclscf  17720  flimfnfcls  17723  fcfnei  17730  alexsublem  17738  alexsubb  17740  alexsubALTlem3  17743  alexsubALTlem4  17744  alexsubALT  17745  tgpt0  17801  divstgplem  17803  tsmsi  17816  tsmssubm  17825  tsmsres  17826  tsmsf1o  17827  tsmsxp  17837  imasdsf1olem  17937  blss  17972  metss  18054  comet  18059  metcnp3  18086  metcnp2  18088  txmetcnp  18093  nrmmetd  18097  nlmvscn  18198  nrginvrcn  18202  nmolb  18226  xrge0tsms  18339  divcn  18372  fsumcn  18374  elcncf2  18394  cncfi  18398  mulc1cncf  18409  cncfco  18411  cncfmet  18412  xrhmeo  18444  bndth  18456  nmoleub2lem2  18597  nmoleub3  18600  ipcn  18673  lmmbr  18684  caucfil  18709  pmltpc  18810  ovolfiniun  18860  ovolicc2lem3  18878  ovolicc2  18881  mblsplit  18891  finiunmbl  18901  volfiniun  18904  voliunlem3  18909  ioorinv  18931  ioorcl  18932  dyadmax  18953  dyadmbllem  18954  dyadmbl  18955  opnmbllem  18956  volcn  18961  vitalilem2  18964  vitalilem3  18965  vitali  18968  i1fd  19036  itg2seq  19097  itg2addlem  19113  itgfsum  19181  ellimc3  19229  dvbsss  19252  dvnres  19280  dvmptfsum  19322  dvferm1lem  19331  dvferm2lem  19333  rolle  19337  c1lip1  19344  lhop1lem  19360  lhop1  19361  dvfsumlem2  19374  dvfsumlem4  19376  dvfsumrlim  19378  dvfsum2  19381  ftc1a  19384  ftc1lem4  19386  ftc1lem6  19388  mpfind  19428  pf1ind  19438  mdegleb  19450  mdeglt  19451  deg1leb  19481  deg1lt  19483  ply1divex  19522  fta1glem2  19552  fta1g  19553  plyco0  19574  plyeq0lem  19592  coeeq2  19624  dgrle  19625  dgrcolem2  19655  dgrco  19656  plydivlem4  19676  plydivex  19677  fta1lem  19687  fta1  19688  vieta1lem2  19691  vieta1  19692  aalioulem2  19713  aalioulem4  19715  abelth  19817  cxpcn3  20088  rlimcnp  20260  xrlimcnp  20263  cxploglim  20272  scvxcvx  20280  jensen  20283  wilthlem2  20307  wilthlem3  20308  fta  20317  dvdsmulf1o  20434  perfectlem2  20469  dchrelbas3  20477  dchrelbas4  20482  dchrn0  20489  bcmono  20516  lgsdir2lem4  20565  lgsdchr  20587  lgseisenlem2  20589  lgsquad2lem2  20598  2sqlem6  20608  2sqlem8  20611  2sqlem10  20613  dchrisumlema  20637  dchrisumlem2  20639  dchrisumlem3  20640  isass  20983  ismgm  20987  isexid2  20992  nvz  21235  nmobndseqi  21357  nmobndseqiOLD  21358  nmlno0  21373  blocnilem  21382  dipdir  21420  dipass  21423  siilem2  21430  ubthlem2  21450  ubth  21452  htth  21498  normpyth  21724  norm3lemt  21731  chlimi  21814  chcompl  21822  omlsii  21982  pjoml  22015  h1de2i  22132  elspansn2  22146  h1datom  22161  pjoml2  22190  pjoml3  22191  lecm  22196  chscllem2  22217  osum  22224  spansncv  22232  pjcjt2  22271  pjopyth  22299  eigre  22415  eigorth  22418  hhcno  22484  hhcnf  22485  cnopc  22493  cnfnc  22510  nmcexi  22606  nmcopexi  22607  nmcfnexi  22631  pjssge0i  22746  hstel2  22799  stj  22815  stri  22837  hstri  22845  stcltr1i  22854  mdbr  22874  mdi  22875  mdbr3  22877  mdbr4  22878  dmdbr  22879  dmdmd  22880  dmdi  22882  dmdbr3  22885  dmdbr4  22886  dmdbr5  22888  mdsl1i  22901  mdslmd1lem3  22907  mdslmd1lem4  22908  mdslmd1i  22909  csmdsymi  22914  cvmd  22916  atss  22926  atom1d  22933  chcv1  22935  hatomic  22940  atord  22968  atcvat2  22969  mddmdin0i  23011  ifeqeqx  23034  rmoxfrdOLD  23146  rmoxfrd  23147  ssiun2sf  23157  fmptcof2  23229  xrge0iifiso  23317  xrge0tsmsd  23382  esumcvg  23454  isrnsigaOLD  23473  sigaclcu  23478  sigaclci  23493  unelsiga  23495  measvun  23537  measiun  23545  subfacp1lem6  23716  erdszelem9  23730  kur14lem9  23745  sconpht  23760  cvmsss2  23805  cvmliftlem7  23822  cvmliftlem10  23825  eupath2  23904  ghomf1olem  24001  relexpsucr  24026  relexpsucl  24028  relexpcnv  24029  relexpdm  24032  relexprn  24033  relexpadd  24035  relexpindlem  24036  rtrclreclem.min  24044  dedekind  24082  dfpo2  24112  fununiq  24126  setinds  24134  dfon2lem3  24141  dfon2lem4  24142  dfon2lem5  24143  dfon2lem6  24144  dfon2lem7  24145  dfon2lem8  24146  dfon2  24148  predbrg  24186  preddowncl  24196  tfisg  24204  wfisg  24209  frmin  24242  frinsg  24245  wfrlem9  24264  frrlem5e  24289  nocvxminlem  24344  funpartfv  24483  axcgrtr  24543  btwnconn1lem11  24720  linethru  24776  rankelg  24798  rankeq1o  24801  fprg  25133  cbcpcp  25162  prjmapcp2  25170  isorhom  25211  preoref22  25229  preotr2  25235  mxlelt  25264  ismxl2  25267  ismnl2  25268  defge3  25271  defse3  25272  inposet  25278  iscom  25333  idlvalNEW  25445  svli2  25484  osneisi  25531  istopx  25547  bwt2  25592  supnuf  25629  supexr  25631  cnegvex2b  25662  rnegvex2b  25663  intvconlem1  25703  isded  25736  dedi  25737  domcmpd  25746  codcmpd  25747  iscatOLD  25754  cati  25755  cmpasso  25773  cmpida  25774  cmpidb  25775  ishomd  25790  ismona  25809  ismonb  25810  ismonb2  25812  cmpmon  25815  isepia  25819  isepib  25820  isepib2  25822  isfuna  25834  isinob  25862  islimcat  25876  tartarmap  25888  rocatval2  25960  setiscat  25979  clscnc  26010  pgapspf2  26053  isig2a2  26066  isibg2  26110  isibg2aa  26112  isibg2aalem1  26113  isibg2aalem2  26114  isibg2aalem3  26115  segline  26141  isibcg  26191  subtr  26224  subtr2  26225  trer  26227  nn0prpwlem  26238  nn0prpw  26239  comppfsc  26307  neibastop2lem  26309  filnetlem4  26330  f1opr  26391  sdclem2  26452  fdc  26455  fdc1  26456  neificl  26467  mettrifi  26473  sstotbnd2  26498  cntotbnd  26520  heibor1lem  26533  bfp  26548  iscringd  26624  ispridl  26659  pridl  26662  ismaxidl  26665  maxidlmax  26668  ispridlc  26695  pridlc  26696  dmnnzd  26700  ismrcd1  26773  ismrcd2  26774  ismrc  26776  isnacs3  26785  nacsfix  26787  mzpcompact2  26830  fphpd  26899  fphpdo  26900  monotuz  27026  monotoddzzfi  27027  monotoddzz  27028  oddcomabszz  27029  zindbi  27031  setindtrs  27118  dford3lem2  27120  ttac  27129  dnnumch1  27141  fnwe2lem2  27148  aomclem3  27153  aomclem6  27156  supeq123d  27158  aomclem8  27159  dfac11  27160  dfac21  27164  islssfg2  27169  frlmup1  27250  lindfrn  27291  islindf4  27308  islindf5  27309  hbtlem5  27332  hbt  27334  flcidc  27379  symggen  27411  psgnunilem4  27420  mendlmod  27501  sdrgacs  27509  pm14.122b  27623  sbiota1  27634  fnchoice  27700  fmul01  27710  fmulcl  27711  fmuldfeqlem1  27712  fmuldfeq  27713  fmul01lt1lem1  27714  fmul01lt1lem2  27715  climmulf  27730  climexp  27731  climsuse  27734  climrecf  27735  climinff  27737  stoweidlem3  27752  stoweidlem4  27753  stoweidlem6  27755  stoweidlem8  27757  stoweidlem15  27764  stoweidlem16  27765  stoweidlem17  27766  stoweidlem19  27768  stoweidlem20  27769  stoweidlem22  27771  stoweidlem23  27772  stoweidlem26  27775  stoweidlem27  27776  stoweidlem30  27779  stoweidlem31  27780  stoweidlem32  27781  stoweidlem34  27783  stoweidlem35  27784  stoweidlem42  27791  stoweidlem43  27792  stoweidlem48  27797  stoweidlem50  27799  stoweidlem51  27800  stoweidlem57  27806  stoweidlem59  27808  stoweidlem62  27811  wallispilem3  27816  sbcfun  27985  nbusgra  28143  frgra3vlem1  28178  3vfriswmgralem  28182  3vfriswmgra  28183  imbi12  28282  sbcssOLD  28306  bnj1385  28865  bnj110  28890  bnj222  28915  bnj229  28916  bnj590  28942  bnj865  28955  bnj849  28957  bnj981  28982  bnj1014  28992  bnj1015  28993  bnj1112  29013  bnj1118  29014  bnj1123  29016  bnj1128  29020  bnj1125  29022  bnj1148  29026  bnj1154  29029  bnj1326  29056  bnj1384  29062  bnj1489  29086  bnj1497  29090  a12lem1  29130  lubunNEW  29163  lshpdisj  29177  lsmsatcv  29200  lsat0cv  29223  lcvexchlem4  29227  lcvexchlem5  29228  l1cvpat  29244  isopos  29370  oposlem  29373  isoml  29428  omllaw  29433  isatl  29489  atlex  29506  iscvlat  29513  cvlexch1  29518  glbconN  29566  hlsuprexch  29570  ps-1  29666  3atlem5  29676  psubspi  29936  llnexchb2  30058  elpcliN  30082  pclfinclN  30139  ldilval  30302  ltrnfset  30306  ltrnset  30307  ltrnu  30310  trlfset  30349  trlset  30350  trlval2  30352  cdleme25cv  30547  cdleme31so  30568  cdleme31fv  30579  cdlemefrs29bpre0  30585  cdleme32fva  30626  cdleme40v  30658  trlord  30758  cdlemkid3N  31122  cdlemkid4  31123  dihffval  31420  dihfval  31421  dihval  31422  lpolconN  31677  mapdordlem2  31827  hdmapfval  32020  hdmapval  32021  hdmapval2  32025
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 177
  Copyright terms: Public domain W3C validator