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

Theorem imbi2d 308
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 23 . 2  |-  ( ph  ->  ( th  ->  ( ps 
<->  ch ) ) )
32pm5.74d 239 1  |-  ( ph  ->  ( ( th  ->  ps )  <->  ( th  ->  ch ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177
This theorem is referenced by:  imbi12d  312  imbi2  315  pm5.42  532  orbi2d  683  con3th  925  19.23tOLD  1834  ax12olem6OLD  1982  ax11v2  2025  ax11v2OLD  2026  ax15  2077  nfsb4t  2137  sbcom  2146  ax11vALT  2154  sbcom2  2171  ax11eq  2251  ax11el  2252  ax11indalem  2255  ax11inda2ALT  2256  ax11inda  2258  ax11v2-o  2259  mo  2284  2mo  2340  2eu6  2347  2gencl  2953  3gencl  2954  vtocl2gf  2981  vtocl3gf  2982  eqeu  3073  mo2icl  3081  euind  3089  reu7  3097  reuind  3105  sbctt  3191  sbcnestgf  3266  r19.36zv  3696  dedth2h  3749  dedth3h  3750  dedth4h  3751  preq12bg  3945  elint  4024  elintrabg  4031  intab  4048  trss  4279  axrep1  4289  axrep2  4290  axrep3  4291  bm1.3ii  4301  pocl  4478  swopolem  4480  solin  4494  freq1  4520  frminex  4530  reusv3  4698  tfisi  4805  tfindsg  4807  tfinds2  4810  tfinds3  4811  dfom2  4814  elom  4815  findsg  4839  finds2  4840  vtoclr  4889  2optocl  4920  3optocl  4921  raliunxp  4981  resieq  5123  iss  5156  cnveqb  5293  funmo  5437  funimaexg  5497  fnbrfvb  5734  fvelimab  5749  fvmptss  5780  fmptco  5868  fprg  5882  fnressn  5885  fressnfv  5887  isoselem  6028  ovg  6179  caovcan  6218  caovordig  6219  caovord  6225  f1o2ndf1  6421  poxp  6425  fnse  6430  riotasvd  6559  riotasvdOLD  6560  smoeq  6579  smores  6581  smogt  6596  tfrlem1  6603  tfr3  6627  oaordi  6756  oeordi  6797  oeoa  6807  oeoe  6809  nnacl  6821  nnmcl  6822  nnecl  6823  nnacom  6827  nnaordi  6828  nnawordi  6831  nnaass  6832  nndi  6833  nnmass  6834  nnmsucr  6835  nnmcom  6836  nnmordi  6841  2ecoptocl  6962  3ecoptocl  6963  th3qlem2  6978  undifixp  7065  xpdom2g  7171  findcard2  7315  xpfi  7345  fnfi  7351  fodomfi  7352  finsschain  7379  marypha1lem  7404  marypha1  7405  supeq1  7416  ordiso2  7448  ordtypelem7  7457  wemaplem1  7479  inf3lem2  7548  inf3lem5  7551  infdiffi  7576  cantnfval2  7588  cantnfle  7590  cantnfp1lem3  7600  oemapval  7603  cantnflem1  7609  cantnf  7613  wemapwe  7618  cnfcom  7621  cnfcom3clem  7626  tz9.1  7629  r1pwOLD  7736  cplem2  7778  karden  7783  infxpenc2lem2  7865  fseqenlem1  7869  dfac8clem  7877  alephinit  7940  dfac4  7967  dfac5lem5  7972  dfac2a  7974  dfac2  7975  dfacacn  7985  dfac12lem3  7989  kmlem2  7995  kmlem13  8006  ackbij1lem16  8079  sornom  8121  infpssrlem4  8150  fin23lem14  8177  fin23lem32  8188  fin23lem34  8190  fin23lem36  8192  isf32lem1  8197  isf32lem2  8198  axcc2lem  8280  axcc3  8282  axcclem  8301  zornn0g  8349  ttukeylem5  8357  ttukeylem6  8358  axrepnd  8433  axpowndlem3  8438  zfcndrep  8453  fpwwe2lem8  8476  pwfseqlem3  8499  wunr1om  8558  wunfi  8560  tskr1om  8606  ingru  8654  grudomon  8656  axgroth3  8670  axgroth4  8671  nqereu  8770  mulcanenq  8801  elnp  8828  elnpi  8829  prlem934  8874  infm3  9931  nnaddcl  9986  nnmulcl  9987  peano5uzi  10322  uzind2  10326  uzindOLD  10328  zindd  10335  eluzadd  10478  uzaddcl  10497  uzwo  10503  uzwoOLD  10504  indstr  10509  zmax  10535  xmulasslem  10828  xrsupsslem  10849  xrinfmsslem  10850  xrsupss  10851  xrinfmss  10852  flval2  11184  om2uzlti  11253  uzrdgfni  11261  seqcl2  11304  seqfveq2  11308  seqshft2  11312  monoord  11316  seqsplit  11319  seqcaopr3  11321  seqf1olem2a  11324  seqf1o  11327  seqid2  11332  seqhomo  11333  ser1const  11342  expcllem  11355  expeq0  11373  mulexp  11382  expadd  11385  expmul  11388  leexp2r  11400  leexp1a  11401  bernneq  11468  modexp  11477  facdiv  11541  faclbnd  11544  faclbnd4lem4  11550  faclbnd6  11553  hashgadd  11614  hashxp  11660  hashmap  11661  hashf1lem2  11668  hashf1  11669  seqcoll  11675  wrdind  11754  cjexp  11918  absexp  12072  rlim  12252  rlim2  12253  rlim0  12265  rlim0lt  12266  rlimi  12270  ello12r  12274  ello1mpt  12278  ello1d  12280  elo12r  12285  lo1o1  12289  o1lo1  12294  lo1res  12316  climshft  12333  o1compt  12344  rlimo1  12373  lo1add  12383  lo1mul  12384  rlimdiv  12402  climub  12418  climserle  12419  caucvgrlem  12429  caurcvgr  12430  iseraltlem2  12439  summolem2a  12472  sumss  12481  fsum2d  12518  fsumabs  12543  fsumrlim  12553  fsumo1  12554  fsumiun  12563  binom  12572  bcxmas  12578  climcndslem1  12592  climcndslem2  12593  cvgrat  12623  demoivreALT  12765  ruclem8  12799  ruclem9  12800  dvdsle  12858  dvdsfac  12867  divalglem7  12882  bitsinv1  12917  sadcadd  12933  sadadd2  12935  saddisjlem  12939  smuval2  12957  smupvallem  12958  smu01lem  12960  smupval  12963  smueqlem  12965  smumullem  12967  bezoutlem4  13004  gcdmultiple  13013  rplpwr  13019  nn0seqcvgd  13024  seq1st  13025  alginv  13029  algcvga  13033  algfx  13034  prmind2  13053  prmdvdsexp  13077  prmfac1  13081  pcmpt  13224  pcfac  13231  prmpwdvds  13235  prmreclem4  13250  vdwlem10  13321  ramval  13339  ramcl  13360  prmlem1a  13392  imasleval  13729  ismre  13778  mreexexd  13836  lubprop  14400  lubid  14402  glbprop  14405  joinlem  14410  meetlem  14417  isglbd  14507  lubun  14513  oduclatb  14534  poslubmo  14536  poslubd  14537  spwmo  14621  spwpr4  14626  frmdgsum  14770  mulgnnass  14881  mhmmulg  14885  gsumwrev  15125  sylow1lem1  15195  efginvrel2  15322  efgsrel  15329  efgredlemd  15339  efgredlem  15342  efgred  15343  efgrelexlemb  15345  gsum2d  15509  gsumcom2  15512  ablfac1eulem  15593  pgpfac1lem2  15596  pgpfac1lem5  15600  pgpfac1  15601  pgpfac  15605  isdomn2  16322  mplcoe1  16491  mplcoe3  16492  mplcoe2  16493  cnfldexp  16697  fiinopn  16937  mretopd  17119  neiptoptop  17158  cnpfval  17260  iscnp3  17270  tgcn  17278  lmbr  17284  lmbr2  17285  lmbrf  17286  lmss  17324  ishaus  17348  hausnei2  17379  t1sep2  17395  fiuncmp  17429  dfcon2  17443  1stcfb  17469  2ndc1stc  17475  1stcrest  17477  1stcelcls  17485  1stccn  17487  lly1stc  17520  elkgen  17529  kgencn  17549  tx1stc  17643  xkopt  17648  cnmptcom  17671  isr0  17730  r0sep  17741  ptcmpfi  17806  isfildlem  17850  rnelfm  17946  fbflim  17969  flimrest  17976  isflf  17986  flffbas  17988  lmflf  17998  fclsrest  18017  isfcf  18027  cnextfvval  18057  tmdmulg  18083  tmdgsum  18086  eltsms  18123  tsmsi  18124  tsmsgsum  18129  tsmssubm  18133  tsmsres  18134  tsmsf1o  18135  isust  18194  isucn  18269  isucn2  18270  ucnima  18272  imasdsf1olem  18364  metss  18499  met1stc  18512  metcnp  18532  metcnpi  18535  metcnpi2  18536  metucnOLD  18579  metucn  18580  xrge0tsms  18826  fsumcn  18861  elcncf  18880  cncfi  18885  rescncf  18888  cncfco  18898  caucfil  19197  equivcau  19214  caubl  19221  caublcls  19222  ovolgelb  19337  ovolunlem1a  19353  ovolicc2lem3  19376  voliunlem1  19405  voliunlem3  19407  volsuplem  19410  volsup  19411  dyadmax  19451  vitali  19466  itg2leub  19587  itgfsum  19679  dvnadd  19776  dvnres  19778  cpnord  19782  dvnfre  19799  dvmptfsum  19820  dvferm1  19830  dvferm2  19832  rolle  19835  dvlip  19838  c1lip1  19842  lhop1  19859  deg1leb  19979  ply1divex  20020  fta1g  20051  plyco  20121  dgrcolem1  20152  dgrco  20154  dvnply2  20165  plydivex  20175  aalioulem2  20211  aalioulem3  20212  aalioulem5  20214  aaliou3lem2  20221  dvntaylp  20248  taylthlem1  20250  ulmdvlem3  20279  abelthlem9  20317  cxpmul2  20541  scvxcvx  20785  jensenlem2  20787  jensen  20788  wilthlem3  20814  perfectlem2  20975  bcmono  21022  bposlem5  21033  lgsquad2lem2  21104  dchrisumlem1  21144  dchrisum0flb  21165  pntpbnd1  21241  pntlemf  21260  qabvle  21280  qabvexp  21281  ostthlem2  21283  ostth2lem2  21289  sizeusglecusglem1  21454  2pthoncl  21564  fargshiftf1  21585  3v3e3cycl1  21592  4cycl4v4e  21614  4cycl4dv4e  21616  eupatrl  21651  eupath2  21663  isplig  21726  gxnn0add  21823  gxnn0mul  21826  ghgrp  21917  ghablo  21918  isnvlem  22050  nvi  22054  nmoubi  22234  nmounbi  22238  nmblolbi  22262  ipasslem1  22293  ipassi  22303  hlim2  22655  pjhth  22856  spansni  23020  elspansn2  23030  pjige0  23154  pjcjt2  23155  pjopyth  23183  elcnop  23321  elcnfn  23346  nmopub  23372  cnopc  23377  nmfnleub  23389  elnlfn  23392  cnfnc  23394  nmbdoplb  23489  nmcexi  23490  nmcoplb  23494  lnfnmul  23512  nmbdfnlb  23514  nmcfnlb  23518  pjss2coi  23628  pjssmi  23629  isst  23677  ishst  23678  stcltr1i  23738  mdbr  23758  dmdbr  23763  mddmd2  23773  mdslmd1lem3  23791  mdslmd1lem4  23792  elat2  23804  atcvat2  23853  cdj1i  23897  iuninc  23972  fmptcof2  24037  xrge0tsmsd  24184  isofld  24196  ofldadd  24199  ofldchr  24205  isarchi2  24216  esumfzf  24420  issiga  24455  isrnsiga  24457  ismeas  24514  isrnmeas  24515  measiun  24533  rrvsum  24673  subfacp1lem6  24832  erdszelem8  24845  isscon  24874  cvmliftlem7  24939  cvmliftlem10  24942  cvmlift3lem2  24968  ghomf1olem  25066  relexp0  25090  relexpsucr  25091  relexpsucl  25093  relexpind  25101  dfrtrclrec2  25104  rtrclreclem.refl  25105  rtrclreclem.subset  25106  rtrclreclem.min  25108  dfrtrcl2  25109  shftvalg  25169  clim2prod  25177  prodfn0  25183  prodfrec  25184  ntrivcvgfvn0  25188  prodmolem2a  25221  fprodabs  25258  fprodefsum  25259  fprodn0  25264  fprod2d  25266  iprodefisumlem  25278  binomfallfac  25316  faclimlem1  25318  dfpo2  25334  rdgprc  25373  preddowncl  25418  trpredmintr  25456  frmin  25464  soseq  25476  wfr3g  25477  wfrlem4  25481  frr3g  25502  bpolycl  26010  bpolydif  26013  fveleq  26113  mbfresfi  26160  itg2gt0cn  26167  sdclem2  26344  fdc  26347  seqpo  26349  incsequz  26350  mettrifi  26361  prdsbnd2  26402  heiborlem4  26421  bfplem1  26429  iscringd  26507  maxidlval  26547  igenval2  26574  ismrc  26653  incssnn0  26663  mzpexpmpt  26700  pell14qrexpclnn0  26827  monotuz  26902  expmordi  26908  rmxypos  26910  jm2.17a  26923  jm2.17b  26924  rmygeid  26927  divalgmodcl  26956  jm2.18  26957  jm2.19lem3  26960  jm2.25  26968  jm2.15nn0  26972  jm2.16nn0  26973  wepwsolem  27014  aomclem8  27035  dfac11  27036  pwslnm  27072  islindf4  27184  lnr2i  27196  hbtlem5  27208  cnsrexpcl  27246  rngunsnply  27254  psgnunilem3  27295  isdomn3  27399  pm14.122b  27499  fnchoice  27575  fmul01  27585  fmuldfeq  27588  climsuselem1  27608  climinff  27612  stoweidlem2  27626  stoweidlem3  27627  stoweidlem17  27641  stoweidlem19  27643  stoweidlem21  27645  stoweidlem26  27650  swrdccatin2  28026  swrdccatin12lem4  28033  swrdccatin12  28034  swrdccat3  28037  usgra2pth  28049  el2wlkonot  28074  el2spthonot  28075  frgra3vlem1  28112  3vfriswmgralem  28116  usg2spot2nb  28176  2spotmdisj  28179  bnj941  28861  bnj106  28957  bnj155  28968  bnj590  28999  bnj591  29000  bnj849  29014  bnj893  29017  bnj944  29027  bnj1128  29077  ax12olem6NEW7  29177  ax11v2NEW7  29246  ax15NEW7  29252  nfsb4twAUX7  29292  sbcomwAUX7  29303  nfsb4tOLD7  29441  nfsb4tw2AUXOLD7  29442  sbcomOLD7  29451  sbcom2OLD7  29457  lubunNEW  29468  isopos  29675  isat3  29802  ishlat1  29847  glbconN  29871  ispsubsp  30239  isldil  30604  isltrn  30613  isdilN  30648  trlval  30656  cdleme27b  30862  cdleme29b  30869  cdleme31sn1  30875  cdleme31sn1c  30882  cdleme40v  30963  cdlemk36  31407  cdlemkid5  31429  cdlemn11pre  31705  dihord2pre  31720  islpolN  31978  hdmapffval  32324  hdmapfval  32325  hdmapval2lem  32329
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 178
  Copyright terms: Public domain W3C validator