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.23t  1798  ax12olem6  1875  ax11v2  1934  ax15  1963  nfsb4t  2022  sbcom  2031  sbcom2  2055  ax11eq  2134  ax11el  2135  ax11indalem  2138  ax11inda2ALT  2139  ax11inda  2141  ax11v2-o  2142  mo  2167  2mo  2223  2eu6  2230  2gencl  2819  3gencl  2820  vtocl2gf  2847  vtocl3gf  2848  eqeu  2938  mo2icl  2946  euind  2954  reu7  2962  reuind  2970  sbctt  3055  sbcnestgf  3130  r19.36zv  3556  dedth2h  3609  dedth3h  3610  dedth4h  3611  preq12bg  3793  elint  3870  elintrabg  3877  intab  3894  trss  4124  axrep1  4134  axrep2  4135  axrep3  4136  bm1.3ii  4146  pocl  4323  swopolem  4325  solin  4339  freq1  4365  frminex  4375  reusv3  4544  tfisi  4651  tfindsg  4653  tfinds2  4656  tfinds3  4657  dfom2  4660  elom  4661  findsg  4685  finds2  4686  vtoclr  4735  2optocl  4767  3optocl  4768  raliunxp  4827  resieq  4967  iss  5000  cnveqb  5131  funmo  5273  funimaexg  5331  fnbrfvb  5565  fvelimab  5580  fvmptss  5611  fmptco  5693  fnressn  5707  fressnfv  5709  f1fveq  5788  isoselem  5840  ovg  5988  caovcan  6026  caovordig  6027  caovord  6033  poxp  6229  fnse  6234  riotasvd  6349  riotasvdOLD  6350  smoeq  6369  smores  6371  smogt  6386  tfrlem1  6393  tfr3  6417  oaordi  6546  oeordi  6587  oeoa  6597  oeoe  6599  nnacl  6611  nnmcl  6612  nnecl  6613  nnacom  6617  nnaordi  6618  nnawordi  6621  nnaass  6622  nndi  6623  nnmass  6624  nnmsucr  6625  nnmcom  6626  nnmordi  6631  2ecoptocl  6751  3ecoptocl  6752  th3qlem2  6767  undifixp  6854  xpdom2g  6960  findcard2  7100  xpfi  7130  fnfi  7136  fodomfi  7137  finsschain  7164  marypha1lem  7188  marypha1  7189  supeq1  7200  ordiso2  7232  ordtypelem7  7241  wemaplem1  7263  inf3lem2  7332  inf3lem5  7335  infdiffi  7360  cantnfval2  7372  cantnfle  7374  cantnfp1lem3  7384  oemapval  7387  cantnflem1  7393  cantnf  7397  wemapwe  7402  cnfcom  7405  cnfcom3clem  7410  tz9.1  7413  r1pwOLD  7520  cplem2  7562  karden  7567  infxpenc2lem2  7649  fseqenlem1  7653  dfac8clem  7661  alephinit  7724  dfac4  7751  dfac5lem5  7756  dfac2a  7758  dfac2  7759  dfacacn  7769  dfac12lem3  7773  kmlem2  7779  kmlem13  7790  ackbij1lem16  7863  sornom  7905  infpssrlem4  7934  fin23lem14  7961  fin23lem32  7972  fin23lem34  7974  fin23lem36  7976  isf32lem1  7981  isf32lem2  7982  axcc2lem  8064  axcc3  8066  axcclem  8085  zornn0g  8134  ttukeylem5  8142  ttukeylem6  8143  axrepnd  8218  axpowndlem3  8223  zfcndrep  8238  fpwwe2lem8  8261  pwfseqlem3  8284  wunr1om  8343  wunfi  8345  tskr1om  8391  ingru  8439  grudomon  8441  axgroth3  8455  axgroth4  8456  nqereu  8555  mulcanenq  8586  elnp  8613  elnpi  8614  prlem934  8659  infm3  9715  nnaddcl  9770  nnmulcl  9771  peano5uzi  10102  uzind2  10106  uzindOLD  10108  zindd  10115  eluzadd  10258  uzaddcl  10277  uzwo  10283  uzwoOLD  10284  indstr  10289  zmax  10315  xmulasslem  10607  xrsupsslem  10627  xrinfmsslem  10628  xrsupss  10629  xrinfmss  10630  flval2  10946  om2uzlti  11015  uzrdgfni  11023  seqcl2  11066  seqfveq2  11070  seqshft2  11074  monoord  11078  seqsplit  11081  seqcaopr3  11083  seqf1olem2a  11086  seqf1o  11089  seqid2  11094  seqhomo  11095  ser1const  11104  expcllem  11116  expeq0  11134  mulexp  11143  expadd  11146  expmul  11149  leexp2r  11161  leexp1a  11162  bernneq  11229  modexp  11238  facdiv  11302  faclbnd  11305  faclbnd4lem4  11311  faclbnd6  11314  hashgadd  11361  hashxp  11388  hashmap  11389  hashf1lem2  11396  hashf1  11397  seqcoll  11403  wrdind  11479  cjexp  11637  absexp  11791  rlim  11971  rlim2  11972  rlim0  11984  rlim0lt  11985  rlimi  11989  ello12r  11993  ello1mpt  11997  ello1d  11999  elo12r  12004  lo1o1  12008  o1lo1  12013  lo1res  12035  climshft  12052  o1compt  12063  rlimo1  12092  lo1add  12102  lo1mul  12103  rlimdiv  12121  climub  12137  climserle  12138  caucvgrlem  12147  caurcvgr  12148  iseraltlem2  12157  summolem2a  12190  sumss  12199  fsum2d  12236  fsumabs  12261  fsumrlim  12271  fsumo1  12272  fsumiun  12281  binom  12290  bcxmas  12296  climcndslem1  12310  climcndslem2  12311  cvgrat  12341  demoivreALT  12483  ruclem8  12517  ruclem9  12518  dvdsle  12576  dvdsfac  12585  divalglem7  12600  bitsinv1  12635  sadcadd  12651  sadadd2  12653  saddisjlem  12657  smuval2  12675  smupvallem  12676  smu01lem  12678  smupval  12681  smueqlem  12683  smumullem  12685  bezoutlem4  12722  gcdmultiple  12731  rplpwr  12737  nn0seqcvgd  12742  seq1st  12743  alginv  12747  algcvga  12751  algfx  12752  prmind2  12771  prmdvdsexp  12795  prmfac1  12799  pcmpt  12942  pcfac  12949  prmpwdvds  12953  prmreclem4  12968  vdwlem10  13039  ramval  13057  ramcl  13078  prmlem1a  13110  imasleval  13445  ismre  13494  mreexexd  13552  lubprop  14116  lubid  14118  glbprop  14121  joinlem  14126  meetlem  14133  isglbd  14223  lubun  14229  oduclatb  14250  poslubmo  14252  poslubd  14253  spwmo  14337  spwpr4  14342  frmdgsum  14486  mulgnnass  14597  mhmmulg  14601  gsumwrev  14841  sylow1lem1  14911  efginvrel2  15038  efgsrel  15045  efgredlemd  15055  efgredlem  15058  efgred  15059  efgrelexlemb  15061  gsum2d  15225  gsumcom2  15228  ablfac1eulem  15309  pgpfac1lem2  15312  pgpfac1lem5  15316  pgpfac1  15317  pgpfac  15321  isdomn2  16042  mplcoe1  16211  mplcoe3  16212  mplcoe2  16213  cnfldexp  16409  fiinopn  16649  mretopd  16831  cnpfval  16966  iscnp3  16976  tgcn  16984  lmbr  16990  lmbr2  16991  lmbrf  16992  lmss  17028  ishaus  17052  hausnei2  17083  t1sep2  17099  fiuncmp  17133  dfcon2  17147  1stcfb  17173  2ndc1stc  17179  1stcrest  17181  1stcelcls  17189  1stccn  17191  lly1stc  17224  elkgen  17233  kgencn  17253  tx1stc  17346  xkopt  17351  cnmptcom  17374  isr0  17430  r0sep  17441  ptcmpfi  17506  isfildlem  17554  rnelfm  17650  fbflim  17673  flimrest  17680  isflf  17690  flffbas  17692  lmflf  17702  fclsrest  17721  isfcf  17731  tmdmulg  17777  tmdgsum  17780  eltsms  17817  tsmsi  17818  tsmsgsum  17823  tsmssubm  17827  tsmsres  17828  tsmsf1o  17829  imasdsf1olem  17939  metss  18056  met1stc  18069  metcnp  18089  metcnpi  18092  metcnpi2  18093  xrge0tsms  18341  fsumcn  18376  elcncf  18395  cncfi  18400  rescncf  18403  cncfco  18413  caucfil  18711  equivcau  18728  caubl  18735  caublcls  18736  ovolgelb  18841  ovolunlem1a  18857  ovolicc2lem3  18880  voliunlem1  18909  voliunlem3  18911  volsuplem  18914  volsup  18915  dyadmax  18955  vitali  18970  itg2leub  19091  itgfsum  19183  dvnadd  19280  dvnres  19282  cpnord  19286  dvnfre  19303  dvmptfsum  19324  dvferm1  19334  dvferm2  19336  rolle  19339  dvlip  19342  c1lip1  19346  lhop1  19363  deg1leb  19483  ply1divex  19524  fta1g  19555  plyco  19625  dgrcolem1  19656  dgrco  19658  dvnply2  19669  plydivex  19679  aalioulem2  19715  aalioulem3  19716  aalioulem5  19718  aaliou3lem2  19725  dvntaylp  19752  taylthlem1  19754  ulmdvlem3  19781  abelthlem9  19818  cxpmul2  20038  scvxcvx  20282  jensenlem2  20284  jensen  20285  wilthlem3  20310  perfectlem2  20471  bcmono  20518  bposlem5  20529  lgsquad2lem2  20600  dchrisumlem1  20640  dchrisum0flb  20661  pntpbnd1  20737  pntlemf  20756  qabvle  20776  qabvexp  20777  ostthlem2  20779  ostth2lem2  20785  isplig  20846  gxnn0add  20943  gxnn0mul  20946  ghgrp  21037  ghablo  21038  isnvlem  21168  nvi  21172  nmoubi  21352  nmounbi  21356  nmblolbi  21380  ipasslem1  21411  ipassi  21421  hlim2  21773  pjhth  21974  spansni  22138  elspansn2  22148  pjige0  22272  pjcjt2  22273  pjopyth  22301  elcnop  22439  elcnfn  22464  nmopub  22490  cnopc  22495  nmfnleub  22507  elnlfn  22510  cnfnc  22512  nmbdoplb  22607  nmcexi  22608  nmcoplb  22612  lnfnmul  22630  nmbdfnlb  22632  nmcfnlb  22636  pjss2coi  22746  pjssmi  22747  isst  22795  ishst  22796  stcltr1i  22856  mdbr  22876  dmdbr  22881  mddmd2  22891  mdslmd1lem3  22909  mdslmd1lem4  22910  elat2  22922  atcvat2  22971  cdj1i  23015  iuninc  23160  fmptcof2  23231  xrge0iifiso  23319  xrge0tsmsd  23384  issiga  23474  isrnsiga  23476  ismeas  23532  isrnmeas  23533  measiun  23547  subfacp1lem6  23718  erdszelem8  23731  isscon  23759  cvmliftlem7  23824  cvmliftlem10  23827  cvmlift3lem2  23853  eupath2  23906  ghomf1olem  24003  relexp0  24027  relexpsucr  24028  relexpsucl  24030  relexpind  24039  dfrtrclrec2  24042  rtrclreclem.refl  24043  rtrclreclem.subset  24044  rtrclreclem.min  24046  dfrtrcl2  24047  dfpo2  24114  rdgprc  24153  preddowncl  24198  trpredmintr  24236  frmin  24244  soseq  24256  wfr3g  24257  wfrlem4  24261  frr3g  24282  bpolycl  24789  bpolydif  24792  fveleq  24892  elintabg  25101  fprg  25144  cbcpcp  25173  prl2  25180  supdef  25273  inposet  25289  rltrran  25425  svs3  25499  lvsovso  25637  addcanri  25677  issubcv  25681  isded  25747  dedi  25748  iscatOLD  25765  cati  25766  isfunb  25846  fnctartar  25918  fnctartar2  25919  prismorcset2  25929  cmpmor  25986  setiscat  25990  isnword  25997  indcls2  26007  clscnc  26021  pgapspf2  26064  bisig0  26073  isibg2  26121  segline  26152  bsstrs  26157  pdiveql  26179  isibcg  26202  sdclem2  26463  fdc  26466  seqpo  26468  incsequz  26469  mettrifi  26484  prdsbnd2  26530  heiborlem4  26549  bfplem1  26557  iscringd  26635  maxidlval  26675  igenval2  26702  ismrc  26787  incssnn0  26797  mzpexpmpt  26834  pell14qrexpclnn0  26962  monotuz  27037  expmordi  27043  rmxypos  27045  jm2.17a  27058  jm2.17b  27059  rmygeid  27062  divalgmodcl  27091  jm2.18  27092  jm2.19lem3  27095  jm2.25  27103  jm2.15nn0  27107  jm2.16nn0  27108  wepwsolem  27149  aomclem8  27170  dfac11  27171  pwslnm  27207  islindf4  27319  lnr2i  27331  hbtlem5  27343  cnsrexpcl  27381  rngunsnply  27389  psgnunilem3  27430  isdomn3  27534  pm14.122b  27634  fnchoice  27711  fmul01  27721  fmuldfeq  27724  climsuselem1  27744  climinff  27748  stoweidlem2  27762  stoweidlem3  27763  stoweidlem17  27777  stoweidlem21  27781  stoweidlem26  27786  nbusgra  28154  frgra3vlem1  28189  3vfriswmgralem  28193  bnj941  28877  bnj106  28973  bnj155  28984  bnj590  29015  bnj591  29016  bnj849  29030  bnj893  29033  bnj944  29043  bnj1128  29093  a12study2  29207  lubunNEW  29236  isopos  29443  isat3  29570  ishlat1  29615  glbconN  29639  ispsubsp  30007  isldil  30372  isltrn  30381  isdilN  30416  trlval  30424  cdleme27b  30630  cdleme29b  30637  cdleme31sn1  30643  cdleme31sn1c  30650  cdleme40v  30731  cdlemk36  31175  cdlemkid5  31197  cdlemn11pre  31473  dihord2pre  31488  islpolN  31746  hdmapffval  32092  hdmapfval  32093  hdmapval2lem  32097
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