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

Theorem imbi2d 307
Description: Deduction adding an antecedent to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
imbid.1  |-  ( ph  ->  ( ps  <->  ch )
)
Assertion
Ref Expression
imbi2d  |-  ( ph  ->  ( ( th  ->  ps )  <->  ( th  ->  ch ) ) )

Proof of Theorem imbi2d
StepHypRef Expression
1 imbid.1 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
21a1d 22 . 2  |-  ( ph  ->  ( th  ->  ( ps 
<->  ch ) ) )
32pm5.74d 238 1  |-  ( ph  ->  ( ( th  ->  ps )  <->  ( th  ->  ch ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176
This theorem is referenced by:  imbi12d  311  imbi2  314  pm5.42  531  orbi2d  682  con3th  924  19.23tOLD  1821  ax12olem6  1937  ax11v2  1997  ax15  2026  nfsb4t  2085  sbcom  2094  ax11vALT  2102  sbcom2  2119  ax11eq  2198  ax11el  2199  ax11indalem  2202  ax11inda2ALT  2203  ax11inda  2205  ax11v2-o  2206  mo  2231  2mo  2287  2eu6  2294  2gencl  2893  3gencl  2894  vtocl2gf  2921  vtocl3gf  2922  eqeu  3012  mo2icl  3020  euind  3028  reu7  3036  reuind  3044  sbctt  3129  sbcnestgf  3204  r19.36zv  3630  dedth2h  3683  dedth3h  3684  dedth4h  3685  preq12bg  3870  elint  3947  elintrabg  3954  intab  3971  trss  4201  axrep1  4211  axrep2  4212  axrep3  4213  bm1.3ii  4223  pocl  4400  swopolem  4402  solin  4416  freq1  4442  frminex  4452  reusv3  4621  tfisi  4728  tfindsg  4730  tfinds2  4733  tfinds3  4734  dfom2  4737  elom  4738  findsg  4762  finds2  4763  vtoclr  4812  2optocl  4844  3optocl  4845  raliunxp  4904  resieq  5044  iss  5077  cnveqb  5208  funmo  5350  funimaexg  5408  fnbrfvb  5643  fvelimab  5658  fvmptss  5689  fmptco  5771  fprg  5785  fnressn  5786  fressnfv  5788  f1fveq  5870  isoselem  5922  ovg  6070  caovcan  6108  caovordig  6109  caovord  6115  poxp  6311  fnse  6316  riotasvd  6431  riotasvdOLD  6432  smoeq  6451  smores  6453  smogt  6468  tfrlem1  6475  tfr3  6499  oaordi  6628  oeordi  6669  oeoa  6679  oeoe  6681  nnacl  6693  nnmcl  6694  nnecl  6695  nnacom  6699  nnaordi  6700  nnawordi  6703  nnaass  6704  nndi  6705  nnmass  6706  nnmsucr  6707  nnmcom  6708  nnmordi  6713  2ecoptocl  6834  3ecoptocl  6835  th3qlem2  6850  undifixp  6937  xpdom2g  7043  findcard2  7185  xpfi  7215  fnfi  7221  fodomfi  7222  finsschain  7249  marypha1lem  7273  marypha1  7274  supeq1  7285  ordiso2  7317  ordtypelem7  7326  wemaplem1  7348  inf3lem2  7417  inf3lem5  7420  infdiffi  7445  cantnfval2  7457  cantnfle  7459  cantnfp1lem3  7469  oemapval  7472  cantnflem1  7478  cantnf  7482  wemapwe  7487  cnfcom  7490  cnfcom3clem  7495  tz9.1  7498  r1pwOLD  7605  cplem2  7647  karden  7652  infxpenc2lem2  7734  fseqenlem1  7738  dfac8clem  7746  alephinit  7809  dfac4  7836  dfac5lem5  7841  dfac2a  7843  dfac2  7844  dfacacn  7854  dfac12lem3  7858  kmlem2  7864  kmlem13  7875  ackbij1lem16  7948  sornom  7990  infpssrlem4  8019  fin23lem14  8046  fin23lem32  8057  fin23lem34  8059  fin23lem36  8061  isf32lem1  8066  isf32lem2  8067  axcc2lem  8149  axcc3  8151  axcclem  8170  zornn0g  8219  ttukeylem5  8227  ttukeylem6  8228  axrepnd  8303  axpowndlem3  8308  zfcndrep  8323  fpwwe2lem8  8346  pwfseqlem3  8369  wunr1om  8428  wunfi  8430  tskr1om  8476  ingru  8524  grudomon  8526  axgroth3  8540  axgroth4  8541  nqereu  8640  mulcanenq  8671  elnp  8698  elnpi  8699  prlem934  8744  infm3  9800  nnaddcl  9855  nnmulcl  9856  peano5uzi  10189  uzind2  10193  uzindOLD  10195  zindd  10202  eluzadd  10345  uzaddcl  10364  uzwo  10370  uzwoOLD  10371  indstr  10376  zmax  10402  xmulasslem  10694  xrsupsslem  10714  xrinfmsslem  10715  xrsupss  10716  xrinfmss  10717  flval2  11033  om2uzlti  11102  uzrdgfni  11110  seqcl2  11153  seqfveq2  11157  seqshft2  11161  monoord  11165  seqsplit  11168  seqcaopr3  11170  seqf1olem2a  11173  seqf1o  11176  seqid2  11181  seqhomo  11182  ser1const  11191  expcllem  11204  expeq0  11222  mulexp  11231  expadd  11234  expmul  11237  leexp2r  11249  leexp1a  11250  bernneq  11317  modexp  11326  facdiv  11390  faclbnd  11393  faclbnd4lem4  11399  faclbnd6  11402  hashgadd  11449  hashxp  11476  hashmap  11477  hashf1lem2  11484  hashf1  11485  seqcoll  11491  wrdind  11567  cjexp  11725  absexp  11879  rlim  12059  rlim2  12060  rlim0  12072  rlim0lt  12073  rlimi  12077  ello12r  12081  ello1mpt  12085  ello1d  12087  elo12r  12092  lo1o1  12096  o1lo1  12101  lo1res  12123  climshft  12140  o1compt  12151  rlimo1  12180  lo1add  12190  lo1mul  12191  rlimdiv  12209  climub  12225  climserle  12226  caucvgrlem  12236  caurcvgr  12237  iseraltlem2  12246  summolem2a  12279  sumss  12288  fsum2d  12325  fsumabs  12350  fsumrlim  12360  fsumo1  12361  fsumiun  12370  binom  12379  bcxmas  12385  climcndslem1  12399  climcndslem2  12400  cvgrat  12430  demoivreALT  12572  ruclem8  12606  ruclem9  12607  dvdsle  12665  dvdsfac  12674  divalglem7  12689  bitsinv1  12724  sadcadd  12740  sadadd2  12742  saddisjlem  12746  smuval2  12764  smupvallem  12765  smu01lem  12767  smupval  12770  smueqlem  12772  smumullem  12774  bezoutlem4  12811  gcdmultiple  12820  rplpwr  12826  nn0seqcvgd  12831  seq1st  12832  alginv  12836  algcvga  12840  algfx  12841  prmind2  12860  prmdvdsexp  12884  prmfac1  12888  pcmpt  13031  pcfac  13038  prmpwdvds  13042  prmreclem4  13057  vdwlem10  13128  ramval  13146  ramcl  13167  prmlem1a  13199  imasleval  13536  ismre  13585  mreexexd  13643  lubprop  14207  lubid  14209  glbprop  14212  joinlem  14217  meetlem  14224  isglbd  14314  lubun  14320  oduclatb  14341  poslubmo  14343  poslubd  14344  spwmo  14428  spwpr4  14433  frmdgsum  14577  mulgnnass  14688  mhmmulg  14692  gsumwrev  14932  sylow1lem1  15002  efginvrel2  15129  efgsrel  15136  efgredlemd  15146  efgredlem  15149  efgred  15150  efgrelexlemb  15152  gsum2d  15316  gsumcom2  15319  ablfac1eulem  15400  pgpfac1lem2  15403  pgpfac1lem5  15407  pgpfac1  15408  pgpfac  15412  isdomn2  16133  mplcoe1  16302  mplcoe3  16303  mplcoe2  16304  cnfldexp  16507  fiinopn  16747  mretopd  16929  cnpfval  17064  iscnp3  17074  tgcn  17082  lmbr  17088  lmbr2  17089  lmbrf  17090  lmss  17126  ishaus  17150  hausnei2  17181  t1sep2  17197  fiuncmp  17231  dfcon2  17245  1stcfb  17271  2ndc1stc  17277  1stcrest  17279  1stcelcls  17287  1stccn  17289  lly1stc  17322  elkgen  17331  kgencn  17351  tx1stc  17444  xkopt  17449  cnmptcom  17472  isr0  17528  r0sep  17539  ptcmpfi  17604  isfildlem  17648  rnelfm  17744  fbflim  17767  flimrest  17774  isflf  17784  flffbas  17786  lmflf  17796  fclsrest  17815  isfcf  17825  tmdmulg  17871  tmdgsum  17874  eltsms  17911  tsmsi  17912  tsmsgsum  17917  tsmssubm  17921  tsmsres  17922  tsmsf1o  17923  imasdsf1olem  18033  metss  18150  met1stc  18163  metcnp  18183  metcnpi  18186  metcnpi2  18187  xrge0tsms  18436  fsumcn  18471  elcncf  18490  cncfi  18495  rescncf  18498  cncfco  18508  caucfil  18807  equivcau  18824  caubl  18831  caublcls  18832  ovolgelb  18937  ovolunlem1a  18953  ovolicc2lem3  18976  voliunlem1  19005  voliunlem3  19007  volsuplem  19010  volsup  19011  dyadmax  19051  vitali  19066  itg2leub  19187  itgfsum  19279  dvnadd  19376  dvnres  19378  cpnord  19382  dvnfre  19399  dvmptfsum  19420  dvferm1  19430  dvferm2  19432  rolle  19435  dvlip  19438  c1lip1  19442  lhop1  19459  deg1leb  19579  ply1divex  19620  fta1g  19651  plyco  19721  dgrcolem1  19752  dgrco  19754  dvnply2  19765  plydivex  19775  aalioulem2  19811  aalioulem3  19812  aalioulem5  19814  aaliou3lem2  19821  dvntaylp  19848  taylthlem1  19850  ulmdvlem3  19879  abelthlem9  19917  cxpmul2  20141  scvxcvx  20385  jensenlem2  20387  jensen  20388  wilthlem3  20414  perfectlem2  20575  bcmono  20622  bposlem5  20633  lgsquad2lem2  20704  dchrisumlem1  20744  dchrisum0flb  20765  pntpbnd1  20841  pntlemf  20860  qabvle  20880  qabvexp  20881  ostthlem2  20883  ostth2lem2  20889  isplig  20950  gxnn0add  21047  gxnn0mul  21050  ghgrp  21141  ghablo  21142  isnvlem  21274  nvi  21278  nmoubi  21458  nmounbi  21462  nmblolbi  21486  ipasslem1  21517  ipassi  21527  hlim2  21879  pjhth  22080  spansni  22244  elspansn2  22254  pjige0  22378  pjcjt2  22379  pjopyth  22407  elcnop  22545  elcnfn  22570  nmopub  22596  cnopc  22601  nmfnleub  22613  elnlfn  22616  cnfnc  22618  nmbdoplb  22713  nmcexi  22714  nmcoplb  22718  lnfnmul  22736  nmbdfnlb  22738  nmcfnlb  22742  pjss2coi  22852  pjssmi  22853  isst  22901  ishst  22902  stcltr1i  22962  mdbr  22982  dmdbr  22987  mddmd2  22997  mdslmd1lem3  23015  mdslmd1lem4  23016  elat2  23028  atcvat2  23077  cdj1i  23121  iuninc  23207  fmptcof2  23277  xrge0tsmsd  23415  neiptoptop  23444  xrge0iifiso  23477  cnextfvval  23502  isust  23509  isucn  23574  ucnima  23576  esumfzf  23725  issiga  23760  isrnsiga  23762  ismeas  23819  isrnmeas  23820  measiun  23836  rrvsum  23961  subfacp1lem6  24120  erdszelem8  24133  isscon  24161  cvmliftlem7  24226  cvmliftlem10  24229  cvmlift3lem2  24255  eupath2  24308  ghomf1olem  24405  relexp0  24429  relexpsucr  24430  relexpsucl  24432  relexpind  24441  dfrtrclrec2  24444  rtrclreclem.refl  24445  rtrclreclem.subset  24446  rtrclreclem.min  24448  dfrtrcl2  24449  shftvalg  24509  clim2prod  24517  prodfn0  24523  prodfrec  24524  ntrivcvgfvn0  24528  prodmolem2a  24561  fprodabs  24598  fprodefsum  24599  fprodn0  24604  risefacn0  24647  gammacvglem1  24651  faclimlem1  24654  dfpo2  24670  rdgprc  24709  preddowncl  24754  trpredmintr  24792  frmin  24800  soseq  24812  wfr3g  24813  wfrlem4  24817  frr3g  24838  bpolycl  25346  bpolydif  25349  fveleq  25449  itg2gt0cn  25495  sdclem2  25776  fdc  25779  seqpo  25781  incsequz  25782  mettrifi  25797  prdsbnd2  25842  heiborlem4  25861  bfplem1  25869  iscringd  25947  maxidlval  25987  igenval2  26014  ismrc  26099  incssnn0  26109  mzpexpmpt  26146  pell14qrexpclnn0  26274  monotuz  26349  expmordi  26355  rmxypos  26357  jm2.17a  26370  jm2.17b  26371  rmygeid  26374  divalgmodcl  26403  jm2.18  26404  jm2.19lem3  26407  jm2.25  26415  jm2.15nn0  26419  jm2.16nn0  26420  wepwsolem  26461  aomclem8  26482  dfac11  26483  pwslnm  26519  islindf4  26631  lnr2i  26643  hbtlem5  26655  cnsrexpcl  26693  rngunsnply  26701  psgnunilem3  26742  isdomn3  26846  pm14.122b  26946  fnchoice  27023  fmul01  27033  fmuldfeq  27036  climsuselem1  27056  climinff  27060  stoweidlem2  27074  stoweidlem3  27075  stoweidlem17  27089  stoweidlem21  27093  stoweidlem26  27098  nbusgra  27586  2pthoncl  27722  fargshiftf1  27743  eupatrl  27746  3v3e3cycl1  27751  4cycl4v4e  27773  4cycl4dv4e  27775  frgra3vlem1  27816  3vfriswmgralem  27820  bnj941  28549  bnj106  28645  bnj155  28656  bnj590  28687  bnj591  28688  bnj849  28702  bnj893  28705  bnj944  28715  bnj1128  28765  ax12olem6NEW7  28865  ax11v2NEW7  28934  ax15NEW7  28940  nfsb4twAUX7  28980  sbcomwAUX7  28991  nfsb4tOLD7  29129  nfsb4tw2AUXOLD7  29130  sbcomOLD7  29139  sbcom2OLD7  29145  a12study2  29186  lubunNEW  29215  isopos  29422  isat3  29549  ishlat1  29594  glbconN  29618  ispsubsp  29986  isldil  30351  isltrn  30360  isdilN  30395  trlval  30403  cdleme27b  30609  cdleme29b  30616  cdleme31sn1  30622  cdleme31sn1c  30629  cdleme40v  30710  cdlemk36  31154  cdlemkid5  31176  cdlemn11pre  31452  dihord2pre  31467  islpolN  31725  hdmapffval  32071  hdmapfval  32072  hdmapval2lem  32076
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