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

Theorem imbi2d 309
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 24 . 2  |-  ( ph  ->  ( th  ->  ( ps 
<->  ch ) ) )
32pm5.74d 240 1  |-  ( ph  ->  ( ( th  ->  ps )  <->  ( th  ->  ch ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178
This theorem is referenced by:  imbi12d  313  imbi2  316  pm5.42  533  orbi2d  684  con3th  926  19.23tOLD  1840  ax12olem6OLD  2019  ax11v2  2081  ax11v2OLD  2082  ax15  2111  nfsb4tOLD  2132  sbcom  2170  sbcomOLD  2171  ax11vALT  2179  sbcom2  2196  ax11eq  2276  ax11el  2277  ax11indalem  2280  ax11inda2ALT  2281  ax11inda  2283  ax11v2-o  2284  mo  2309  2mo  2365  2eu6  2372  2gencl  2991  3gencl  2992  vtocl2gf  3019  vtocl3gf  3020  eqeu  3111  mo2icl  3119  euind  3127  reu7  3135  reuind  3143  sbctt  3236  sbcnestgf  3666  r19.36zv  3752  dedth2h  3805  dedth3h  3806  dedth4h  3807  preq12bg  4001  elint  4080  elintrabg  4087  intab  4104  trss  4336  axrep1  4346  axrep2  4347  axrep3  4348  bm1.3ii  4358  pocl  4539  swopolem  4541  solin  4555  freq1  4581  frminex  4591  reusv3  4760  tfisi  4867  tfindsg  4869  tfinds2  4872  tfinds3  4873  dfom2  4876  elom  4877  findsg  4901  finds2  4902  vtoclr  4951  2optocl  4982  3optocl  4983  raliunxp  5043  resieq  5185  iss  5218  cnveqb  5355  funmo  5499  funimaexg  5559  fnbrfvb  5796  fvelimab  5811  fvmptss  5842  fmptco  5930  fprg  5944  fnressn  5947  fressnfv  5949  isoselem  6090  ovg  6241  caovcan  6280  caovordig  6281  caovord  6287  f1o2ndf1  6483  poxp  6487  fnse  6492  riotasvd  6621  riotasvdOLD  6622  smoeq  6641  smores  6643  smogt  6658  tfrlem1  6665  tfr3  6689  oaordi  6818  oeordi  6859  oeoa  6869  oeoe  6871  nnacl  6883  nnmcl  6884  nnecl  6885  nnacom  6889  nnaordi  6890  nnawordi  6893  nnaass  6894  nndi  6895  nnmass  6896  nnmsucr  6897  nnmcom  6898  nnmordi  6903  2ecoptocl  7024  3ecoptocl  7025  th3qlem2  7040  undifixp  7127  xpdom2g  7233  findcard2  7377  xpfi  7407  fnfi  7413  fodomfi  7414  finsschain  7442  marypha1lem  7467  marypha1  7468  supeq1  7479  ordiso2  7513  ordtypelem7  7522  wemaplem1  7544  inf3lem2  7613  inf3lem5  7616  infdiffi  7641  cantnfval2  7653  cantnfle  7655  cantnfp1lem3  7665  oemapval  7668  cantnflem1  7674  cantnf  7678  wemapwe  7683  cnfcom  7686  cnfcom3clem  7691  tz9.1  7694  r1pwOLD  7801  cplem2  7845  karden  7850  infxpenc2lem2  7932  fseqenlem1  7936  dfac8clem  7944  alephinit  8007  dfac4  8034  dfac5lem5  8039  dfac2a  8041  dfac2  8042  dfacacn  8052  dfac12lem3  8056  kmlem2  8062  kmlem13  8073  ackbij1lem16  8146  sornom  8188  infpssrlem4  8217  fin23lem14  8244  fin23lem32  8255  fin23lem34  8257  fin23lem36  8259  isf32lem1  8264  isf32lem2  8265  axcc2lem  8347  axcc3  8349  axcclem  8368  zornn0g  8416  ttukeylem5  8424  ttukeylem6  8425  axrepnd  8500  axpowndlem3  8505  zfcndrep  8520  fpwwe2lem8  8543  pwfseqlem3  8566  wunr1om  8625  wunfi  8627  tskr1om  8673  ingru  8721  grudomon  8723  axgroth3  8737  axgroth4  8738  nqereu  8837  mulcanenq  8868  elnp  8895  elnpi  8896  prlem934  8941  infm3  9998  nnaddcl  10053  nnmulcl  10054  peano5uzi  10389  uzind2  10393  uzindOLD  10395  zindd  10402  eluzadd  10545  uzaddcl  10564  uzwo  10570  uzwoOLD  10571  indstr  10576  zmax  10602  xmulasslem  10895  xrsupsslem  10916  xrinfmsslem  10917  xrsupss  10918  xrinfmss  10919  flval2  11252  om2uzlti  11321  uzrdgfni  11329  seqcl2  11372  seqfveq2  11376  seqshft2  11380  monoord  11384  seqsplit  11387  seqcaopr3  11389  seqf1olem2a  11392  seqf1o  11395  seqid2  11400  seqhomo  11401  ser1const  11410  expcllem  11423  expeq0  11441  mulexp  11450  expadd  11453  expmul  11456  leexp2r  11468  leexp1a  11469  bernneq  11536  modexp  11545  facdiv  11609  faclbnd  11612  faclbnd4lem4  11618  faclbnd6  11621  hashgadd  11682  hashxp  11728  hashmap  11729  hashf1lem2  11736  hashf1  11737  seqcoll  11743  wrdind  11822  cjexp  11986  absexp  12140  rlim  12320  rlim2  12321  rlim0  12333  rlim0lt  12334  rlimi  12338  ello12r  12342  ello1mpt  12346  ello1d  12348  elo12r  12353  lo1o1  12357  o1lo1  12362  lo1res  12384  climshft  12401  o1compt  12412  rlimo1  12441  lo1add  12451  lo1mul  12452  rlimdiv  12470  climub  12486  climserle  12487  caucvgrlem  12497  caurcvgr  12498  iseraltlem2  12507  summolem2a  12540  sumss  12549  fsum2d  12586  fsumabs  12611  fsumrlim  12621  fsumo1  12622  fsumiun  12631  binom  12640  bcxmas  12646  climcndslem1  12660  climcndslem2  12661  cvgrat  12691  demoivreALT  12833  ruclem8  12867  ruclem9  12868  dvdsle  12926  dvdsfac  12935  divalglem7  12950  bitsinv1  12985  sadcadd  13001  sadadd2  13003  saddisjlem  13007  smuval2  13025  smupvallem  13026  smu01lem  13028  smupval  13031  smueqlem  13033  smumullem  13035  bezoutlem4  13072  gcdmultiple  13081  rplpwr  13087  nn0seqcvgd  13092  seq1st  13093  alginv  13097  algcvga  13101  algfx  13102  prmind2  13121  prmdvdsexp  13145  prmfac1  13149  pcmpt  13292  pcfac  13299  prmpwdvds  13303  prmreclem4  13318  vdwlem10  13389  ramval  13407  ramcl  13428  prmlem1a  13460  imasleval  13797  ismre  13846  mreexexd  13904  lubprop  14468  lubid  14470  glbprop  14473  joinlem  14478  meetlem  14485  isglbd  14575  lubun  14581  oduclatb  14602  poslubmo  14604  poslubd  14605  spwmo  14689  spwpr4  14694  frmdgsum  14838  mulgnnass  14949  mhmmulg  14953  gsumwrev  15193  sylow1lem1  15263  efginvrel2  15390  efgsrel  15397  efgredlemd  15407  efgredlem  15410  efgred  15411  efgrelexlemb  15413  gsum2d  15577  gsumcom2  15580  ablfac1eulem  15661  pgpfac1lem2  15664  pgpfac1lem5  15668  pgpfac1  15669  pgpfac  15673  isdomn2  16390  mplcoe1  16559  mplcoe3  16560  mplcoe2  16561  cnfldexp  16765  fiinopn  17005  mretopd  17187  neiptoptop  17226  cnpfval  17329  iscnp3  17339  tgcn  17347  lmbr  17353  lmbr2  17354  lmbrf  17355  lmss  17393  ishaus  17417  hausnei2  17448  t1sep2  17464  fiuncmp  17498  dfcon2  17513  1stcfb  17539  2ndc1stc  17545  1stcrest  17547  1stcelcls  17555  1stccn  17557  lly1stc  17590  elkgen  17599  kgencn  17619  tx1stc  17713  xkopt  17718  cnmptcom  17741  isr0  17800  r0sep  17811  ptcmpfi  17876  isfildlem  17920  rnelfm  18016  fbflim  18039  flimrest  18046  isflf  18056  flffbas  18058  lmflf  18068  fclsrest  18087  isfcf  18097  cnextfvval  18127  tmdmulg  18153  tmdgsum  18156  eltsms  18193  tsmsi  18194  tsmsgsum  18199  tsmssubm  18203  tsmsres  18204  tsmsf1o  18205  isust  18264  isucn  18339  isucn2  18340  ucnima  18342  imasdsf1olem  18434  metss  18569  met1stc  18582  metcnp  18602  metcnpi  18605  metcnpi2  18606  metucnOLD  18649  metucn  18650  xrge0tsms  18896  fsumcn  18931  elcncf  18950  cncfi  18955  rescncf  18958  cncfco  18968  caucfil  19267  equivcau  19284  caubl  19291  caublcls  19292  ovolgelb  19407  ovolunlem1a  19423  ovolicc2lem3  19446  voliunlem1  19475  voliunlem3  19477  volsuplem  19480  volsup  19481  dyadmax  19521  vitali  19536  itg2leub  19655  itgfsum  19747  dvnadd  19846  dvnres  19848  cpnord  19852  dvnfre  19869  dvmptfsum  19890  dvferm1  19900  dvferm2  19902  rolle  19905  dvlip  19908  c1lip1  19912  lhop1  19929  deg1leb  20049  ply1divex  20090  fta1g  20121  plyco  20191  dgrcolem1  20222  dgrco  20224  dvnply2  20235  plydivex  20245  aalioulem2  20281  aalioulem3  20282  aalioulem5  20284  aaliou3lem2  20291  dvntaylp  20318  taylthlem1  20320  ulmdvlem3  20349  abelthlem9  20387  cxpmul2  20611  scvxcvx  20855  jensenlem2  20857  jensen  20858  wilthlem3  20884  perfectlem2  21045  bcmono  21092  bposlem5  21103  lgsquad2lem2  21174  dchrisumlem1  21214  dchrisum0flb  21235  pntpbnd1  21311  pntlemf  21330  qabvle  21350  qabvexp  21351  ostthlem2  21353  ostth2lem2  21359  sizeusglecusglem1  21524  2pthoncl  21634  fargshiftf1  21655  3v3e3cycl1  21662  4cycl4v4e  21684  4cycl4dv4e  21686  eupatrl  21721  eupath2  21733  isplig  21796  gxnn0add  21893  gxnn0mul  21896  ghgrp  21987  ghablo  21988  isnvlem  22120  nvi  22124  nmoubi  22304  nmounbi  22308  nmblolbi  22332  ipasslem1  22363  ipassi  22373  hlim2  22725  pjhth  22926  spansni  23090  elspansn2  23100  pjige0  23224  pjcjt2  23225  pjopyth  23253  elcnop  23391  elcnfn  23416  nmopub  23442  cnopc  23447  nmfnleub  23459  elnlfn  23462  cnfnc  23464  nmbdoplb  23559  nmcexi  23560  nmcoplb  23564  lnfnmul  23582  nmbdfnlb  23584  nmcfnlb  23588  pjss2coi  23698  pjssmi  23699  isst  23747  ishst  23748  stcltr1i  23808  mdbr  23828  dmdbr  23833  mddmd2  23843  mdslmd1lem3  23861  mdslmd1lem4  23862  elat2  23874  atcvat2  23923  cdj1i  23967  iuninc  24042  fmptcof2  24107  xrge0tsmsd  24254  isofld  24266  ofldadd  24269  ofldchr  24275  isarchi2  24286  esumfzf  24490  issiga  24525  isrnsiga  24527  ismeas  24584  isrnmeas  24585  measiun  24603  rrvsum  24743  subfacp1lem6  24902  erdszelem8  24915  isscon  24944  cvmliftlem7  25009  cvmliftlem10  25012  cvmlift3lem2  25038  ghomf1olem  25136  relexp0  25160  relexpsucr  25161  relexpsucl  25163  relexpind  25171  dfrtrclrec2  25174  rtrclreclem.refl  25175  rtrclreclem.subset  25176  rtrclreclem.min  25178  dfrtrcl2  25179  shftvalg  25239  clim2prod  25247  prodfn0  25253  prodfrec  25254  ntrivcvgfvn0  25258  prodmolem2a  25291  fprodabs  25328  fprodefsum  25329  fprodn0  25334  fprod2d  25336  iprodefisumlem  25348  binomfallfac  25388  faclimlem1  25393  dfpo2  25409  rdgprc  25453  preddowncl  25502  trpredmintr  25540  frmin  25548  soseq  25560  wfr3g  25568  wfrlem4  25572  frr3g  25612  bpolycl  26129  bpolydif  26132  fveleq  26232  heicant  26277  mbfresfi  26289  itg2gt0cn  26298  sdclem2  26484  fdc  26487  seqpo  26489  incsequz  26490  mettrifi  26501  prdsbnd2  26542  heiborlem4  26561  bfplem1  26569  iscringd  26647  maxidlval  26687  igenval2  26714  ismrc  26793  incssnn0  26803  mzpexpmpt  26840  pell14qrexpclnn0  26967  monotuz  27042  expmordi  27048  rmxypos  27050  jm2.17a  27063  jm2.17b  27064  rmygeid  27067  divalgmodcl  27096  jm2.18  27097  jm2.19lem3  27100  jm2.25  27108  jm2.15nn0  27112  jm2.16nn0  27113  wepwsolem  27154  aomclem8  27174  dfac11  27175  pwslnm  27211  islindf4  27323  lnr2i  27335  hbtlem5  27347  cnsrexpcl  27385  rngunsnply  27393  psgnunilem3  27434  isdomn3  27538  pm14.122b  27638  fnchoice  27714  fmul01  27724  fmuldfeq  27727  climsuselem1  27747  climinff  27751  stoweidlem2  27765  stoweidlem3  27766  stoweidlem17  27780  stoweidlem19  27782  stoweidlem21  27784  stoweidlem26  27789  2ffzoeq  28187  swrdccatin12lem4  28271  reumodprminv  28285  cshweqrep  28332  cshwssizesame  28346  usgra2pth  28373  wlkiswwlk2lem4  28400  wlkiswwlk2  28403  el2wlkonot  28425  el2spthonot  28426  frgra3vlem1  28488  3vfriswmgralem  28492  usg2spot2nb  28552  2spotmdisj  28555  bnj941  29241  bnj106  29337  bnj155  29348  bnj590  29379  bnj591  29380  bnj849  29394  bnj893  29397  bnj944  29407  bnj1128  29457  ax12olem6NEW7  29557  ax11v2NEW7  29628  ax15NEW7  29634  nfsb4twAUX7  29674  sbcomwAUX7  29686  sbcom2NEW7  29742  nfsb4tOLD7  29843  nfsb4tw2AUXOLD7  29844  sbcomOLD7  29853  lubunNEW  29869  isopos  30076  isat3  30203  ishlat1  30248  glbconN  30272  ispsubsp  30640  isldil  31005  isltrn  31014  isdilN  31049  trlval  31057  cdleme27b  31263  cdleme29b  31270  cdleme31sn1  31276  cdleme31sn1c  31283  cdleme40v  31364  cdlemk36  31808  cdlemkid5  31830  cdlemn11pre  32106  dihord2pre  32121  islpolN  32379  hdmapffval  32725  hdmapfval  32726  hdmapval2lem  32730
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 179
  Copyright terms: Public domain W3C validator