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  1935  ax15  1966  nfsb4t  2019  sbcom  2028  sbcom2  2056  ax11eq  2133  ax11el  2134  ax11indalem  2137  ax11inda2ALT  2138  ax11inda  2140  ax11v2-o  2141  mo  2166  2mo  2222  2eu6  2229  2gencl  2818  3gencl  2819  vtocl2gf  2846  vtocl3gf  2847  eqeu  2937  mo2icl  2945  euind  2953  reu7  2961  reuind  2969  sbctt  3054  sbcnestgf  3129  r19.36zv  3555  dedth2h  3608  dedth3h  3609  dedth4h  3610  preq12bg  3792  elint  3869  elintrabg  3876  intab  3893  trss  4123  axrep1  4133  axrep2  4134  axrep3  4135  bm1.3ii  4145  pocl  4320  swopolem  4322  solin  4336  freq1  4362  frminex  4372  reusv3  4541  tfisi  4648  tfindsg  4650  tfinds2  4653  tfinds3  4654  dfom2  4657  elom  4658  findsg  4682  finds2  4683  vtoclr  4732  2optocl  4764  3optocl  4765  raliunxp  4824  resieq  4964  iss  4997  cnveqb  5128  funmo  5237  funimaexg  5295  fnbrfvb  5525  fvelimab  5540  fvmptss  5571  fmptco  5653  fnressn  5667  fressnfv  5669  f1fveq  5748  isoselem  5800  ovg  5948  caovcan  5986  caovordig  5987  caovord  5993  poxp  6189  fnse  6194  riotasvd  6343  riotasvdOLD  6344  smoeq  6363  smores  6365  smogt  6380  tfrlem1  6387  tfr3  6411  oaordi  6540  oeordi  6581  oeoa  6591  oeoe  6593  nnacl  6605  nnmcl  6606  nnecl  6607  nnacom  6611  nnaordi  6612  nnawordi  6615  nnaass  6616  nndi  6617  nnmass  6618  nnmsucr  6619  nnmcom  6620  nnmordi  6625  2ecoptocl  6745  3ecoptocl  6746  th3qlem2  6761  undifixp  6848  xpdom2g  6954  findcard2  7094  xpfi  7124  fnfi  7130  fodomfi  7131  finsschain  7158  marypha1lem  7182  marypha1  7183  supeq1  7194  ordiso2  7226  ordtypelem7  7235  wemaplem1  7257  inf3lem2  7326  inf3lem5  7329  infdiffi  7354  cantnfval2  7366  cantnfle  7368  cantnfp1lem3  7378  oemapval  7381  cantnflem1  7387  cantnf  7391  wemapwe  7396  cnfcom  7399  cnfcom3clem  7404  tz9.1  7407  r1pwOLD  7514  cplem2  7556  karden  7561  infxpenc2lem2  7643  fseqenlem1  7647  dfac8clem  7655  alephinit  7718  dfac4  7745  dfac5lem5  7750  dfac2a  7752  dfac2  7753  dfacacn  7763  dfac12lem3  7767  kmlem2  7773  kmlem13  7784  ackbij1lem16  7857  sornom  7899  infpssrlem4  7928  fin23lem14  7955  fin23lem32  7966  fin23lem34  7968  fin23lem36  7970  isf32lem1  7975  isf32lem2  7976  axcc2lem  8058  axcc3  8060  axcclem  8079  zornn0g  8128  ttukeylem5  8136  ttukeylem6  8137  axrepnd  8212  axpowndlem3  8217  zfcndrep  8232  fpwwe2lem8  8255  pwfseqlem3  8278  wunr1om  8337  wunfi  8339  tskr1om  8385  ingru  8433  grudomon  8435  axgroth3  8449  axgroth4  8450  nqereu  8549  mulcanenq  8580  elnp  8607  elnpi  8608  prlem934  8653  infm3  9709  nnaddcl  9764  nnmulcl  9765  peano5uzi  10096  uzind2  10100  uzindOLD  10102  zindd  10109  eluzadd  10252  uzaddcl  10271  uzwo  10277  uzwoOLD  10278  indstr  10283  zmax  10309  xmulasslem  10601  xrsupsslem  10621  xrinfmsslem  10622  xrsupss  10623  xrinfmss  10624  flval2  10940  om2uzlti  11009  uzrdgfni  11017  seqcl2  11060  seqfveq2  11064  seqshft2  11068  monoord  11072  seqsplit  11075  seqcaopr3  11077  seqf1olem2a  11080  seqf1o  11083  seqid2  11088  seqhomo  11089  ser1const  11098  expcllem  11110  expeq0  11128  mulexp  11137  expadd  11140  expmul  11143  leexp2r  11155  leexp1a  11156  bernneq  11223  modexp  11232  facdiv  11296  faclbnd  11299  faclbnd4lem4  11305  faclbnd6  11308  hashgadd  11355  hashxp  11382  hashmap  11383  hashf1lem2  11390  hashf1  11391  seqcoll  11397  wrdind  11473  cjexp  11631  absexp  11785  rlim  11965  rlim2  11966  rlim0  11978  rlim0lt  11979  rlimi  11983  ello12r  11987  ello1mpt  11991  ello1d  11993  elo12r  11998  lo1o1  12002  o1lo1  12007  lo1res  12029  climshft  12046  o1compt  12057  rlimo1  12086  lo1add  12096  lo1mul  12097  rlimdiv  12115  climub  12131  climserle  12132  caucvgrlem  12141  caurcvgr  12142  iseraltlem2  12151  summolem2a  12184  sumss  12193  fsum2d  12230  fsumabs  12255  fsumrlim  12265  fsumo1  12266  fsumiun  12275  binom  12284  bcxmas  12290  climcndslem1  12304  climcndslem2  12305  cvgrat  12335  demoivreALT  12477  ruclem8  12511  ruclem9  12512  dvdsle  12570  dvdsfac  12579  divalglem7  12594  bitsinv1  12629  sadcadd  12645  sadadd2  12647  saddisjlem  12651  smuval2  12669  smupvallem  12670  smu01lem  12672  smupval  12675  smueqlem  12677  smumullem  12679  bezoutlem4  12716  gcdmultiple  12725  rplpwr  12731  nn0seqcvgd  12736  seq1st  12737  alginv  12741  algcvga  12745  algfx  12746  prmind2  12765  prmdvdsexp  12789  prmfac1  12793  pcmpt  12936  pcfac  12943  prmpwdvds  12947  prmreclem4  12962  vdwlem10  13033  ramval  13051  ramcl  13072  prmlem1a  13104  imasleval  13439  ismre  13488  mreexexd  13546  lubprop  14110  lubid  14112  glbprop  14115  joinlem  14120  meetlem  14127  isglbd  14217  lubun  14223  oduclatb  14244  poslubmo  14246  poslubd  14247  spwmo  14331  spwpr4  14336  frmdgsum  14480  mulgnnass  14591  mhmmulg  14595  gsumwrev  14835  sylow1lem1  14905  efginvrel2  15032  efgsrel  15039  efgredlemd  15049  efgredlem  15052  efgred  15053  efgrelexlemb  15055  gsum2d  15219  gsumcom2  15222  ablfac1eulem  15303  pgpfac1lem2  15306  pgpfac1lem5  15310  pgpfac1  15311  pgpfac  15315  isdomn2  16036  mplcoe1  16205  mplcoe3  16206  mplcoe2  16207  cnfldexp  16403  fiinopn  16643  mretopd  16825  cnpfval  16960  iscnp3  16970  tgcn  16978  lmbr  16984  lmbr2  16985  lmbrf  16986  lmss  17022  ishaus  17046  hausnei2  17077  t1sep2  17093  fiuncmp  17127  dfcon2  17141  1stcfb  17167  2ndc1stc  17173  1stcrest  17175  1stcelcls  17183  1stccn  17185  lly1stc  17218  elkgen  17227  kgencn  17247  tx1stc  17340  xkopt  17345  cnmptcom  17368  isr0  17424  r0sep  17435  ptcmpfi  17500  isfildlem  17548  rnelfm  17644  fbflim  17667  flimrest  17674  isflf  17684  flffbas  17686  lmflf  17696  fclsrest  17715  isfcf  17725  tmdmulg  17771  tmdgsum  17774  eltsms  17811  tsmsi  17812  tsmsgsum  17817  tsmssubm  17821  tsmsres  17822  tsmsf1o  17823  imasdsf1olem  17933  metss  18050  met1stc  18063  metcnp  18083  metcnpi  18086  metcnpi2  18087  xrge0tsms  18335  fsumcn  18370  elcncf  18389  cncfi  18394  rescncf  18397  cncfco  18407  caucfil  18705  equivcau  18722  caubl  18729  caublcls  18730  ovolgelb  18835  ovolunlem1a  18851  ovolicc2lem3  18874  voliunlem1  18903  voliunlem3  18905  volsuplem  18908  volsup  18909  dyadmax  18949  vitali  18964  itg2leub  19085  itgfsum  19177  dvnadd  19274  dvnres  19276  cpnord  19280  dvnfre  19297  dvmptfsum  19318  dvferm1  19328  dvferm2  19330  rolle  19333  dvlip  19336  c1lip1  19340  lhop1  19357  deg1leb  19477  ply1divex  19518  fta1g  19549  plyco  19619  dgrcolem1  19650  dgrco  19652  dvnply2  19663  plydivex  19673  aalioulem2  19709  aalioulem3  19710  aalioulem5  19712  aaliou3lem2  19719  dvntaylp  19746  taylthlem1  19748  ulmdvlem3  19775  abelthlem9  19812  cxpmul2  20032  scvxcvx  20276  jensenlem2  20278  jensen  20279  wilthlem3  20304  perfectlem2  20465  bcmono  20512  bposlem5  20523  lgsquad2lem2  20594  dchrisumlem1  20634  dchrisum0flb  20655  pntpbnd1  20731  pntlemf  20750  qabvle  20770  qabvexp  20771  ostthlem2  20773  ostth2lem2  20779  isplig  20838  gxnn0add  20935  gxnn0mul  20938  ghgrp  21029  ghablo  21030  isnvlem  21160  nvi  21164  nmoubi  21344  nmounbi  21348  nmblolbi  21372  ipasslem1  21403  ipassi  21413  hlim2  21767  pjhth  21968  spansni  22132  elspansn2  22142  pjige0  22266  pjcjt2  22267  pjopyth  22295  elcnop  22433  elcnfn  22458  nmopub  22484  cnopc  22489  nmfnleub  22501  elnlfn  22504  cnfnc  22506  nmbdoplb  22601  nmcexi  22602  nmcoplb  22606  lnfnmul  22624  nmbdfnlb  22626  nmcfnlb  22630  pjss2coi  22740  pjssmi  22741  isst  22789  ishst  22790  stcltr1i  22850  mdbr  22870  dmdbr  22875  mddmd2  22885  mdslmd1lem3  22903  mdslmd1lem4  22904  elat2  22916  atcvat2  22965  cdj1i  23009  subfacp1lem6  23123  erdszelem8  23136  isscon  23164  cvmliftlem7  23229  cvmliftlem10  23232  cvmlift3lem2  23258  eupath2  23311  ghomf1olem  23408  relexp0  23432  relexpsucr  23433  relexpsucl  23435  relexpind  23444  dfrtrclrec2  23447  rtrclreclem.refl  23448  rtrclreclem.subset  23449  rtrclreclem.min  23451  dfrtrcl2  23452  dfpo2  23518  rdgprc  23555  preddowncl  23600  trpredmintr  23638  frmin  23646  soseq  23658  wfr3g  23659  wfrlem4  23663  frr3g  23684  elfuns  23864  bpolycl  24197  bpolydif  24200  fveleq  24300  elintabg  24500  fprg  24544  cbcpcp  24573  prl2  24580  supdef  24673  inposet  24689  rltrran  24825  svs3  24899  lvsovso  25037  addcanri  25077  issubcv  25081  isded  25147  dedi  25148  iscatOLD  25165  cati  25166  isfunb  25246  fnctartar  25318  fnctartar2  25319  prismorcset2  25329  cmpmor  25386  setiscat  25390  isnword  25397  indcls2  25407  clscnc  25421  pgapspf2  25464  bisig0  25473  isibg2  25521  segline  25552  bsstrs  25557  pdiveql  25579  isibcg  25602  sdclem2  25863  fdc  25866  seqpo  25868  incsequz  25869  mettrifi  25884  prdsbnd2  25930  heiborlem4  25949  bfplem1  25957  iscringd  26035  maxidlval  26075  igenval2  26102  ismrc  26187  incssnn0  26197  mzpexpmpt  26234  pell14qrexpclnn0  26362  monotuz  26437  expmordi  26443  rmxypos  26445  jm2.17a  26458  jm2.17b  26459  rmygeid  26462  divalgmodcl  26491  jm2.18  26492  jm2.19lem3  26495  jm2.25  26503  jm2.15nn0  26507  jm2.16nn0  26508  wepwsolem  26549  aomclem8  26570  dfac11  26571  pwslnm  26607  islindf4  26719  lnr2i  26731  hbtlem5  26743  cnsrexpcl  26781  rngunsnply  26789  psgnunilem3  26830  isdomn3  26934  pm14.122b  27034  fnchoice  27111  fmul01  27121  fmuldfeq  27124  climsuselem1  27144  climinff  27148  stoweidlem2  27162  stoweidlem3  27163  stoweidlem17  27177  stoweidlem21  27181  stoweidlem26  27186  bnj941  28083  bnj106  28179  bnj155  28190  bnj590  28221  bnj591  28222  bnj849  28236  bnj893  28239  bnj944  28249  bnj1128  28299  a12study2  28413  lubunNEW  28442  isopos  28649  isat3  28776  ishlat1  28821  glbconN  28845  ispsubsp  29213  isldil  29578  isltrn  29587  isdilN  29622  trlval  29630  cdleme27b  29836  cdleme29b  29843  cdleme31sn1  29849  cdleme31sn1c  29856  cdleme40v  29937  cdlemk36  30381  cdlemkid5  30403  cdlemn11pre  30679  dihord2pre  30694  islpolN  30952  hdmapffval  31298  hdmapfval  31299  hdmapval2lem  31303
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