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  1839  ax12olem6OLD  2017  ax11v2  2079  ax11v2OLD  2080  ax15  2109  nfsb4tOLD  2130  sbcom  2166  sbcomOLD  2167  ax11vALT  2175  sbcom2  2192  ax11eq  2272  ax11el  2273  ax11indalem  2276  ax11inda2ALT  2277  ax11inda  2279  ax11v2-o  2280  mo  2305  2mo  2361  2eu6  2368  2gencl  2987  3gencl  2988  vtocl2gf  3015  vtocl3gf  3016  eqeu  3107  mo2icl  3115  euind  3123  reu7  3131  reuind  3139  sbctt  3225  sbcnestgf  3300  r19.36zv  3730  dedth2h  3783  dedth3h  3784  dedth4h  3785  preq12bg  3979  elint  4058  elintrabg  4065  intab  4082  trss  4314  axrep1  4324  axrep2  4325  axrep3  4326  bm1.3ii  4336  pocl  4513  swopolem  4515  solin  4529  freq1  4555  frminex  4565  reusv3  4734  tfisi  4841  tfindsg  4843  tfinds2  4846  tfinds3  4847  dfom2  4850  elom  4851  findsg  4875  finds2  4876  vtoclr  4925  2optocl  4956  3optocl  4957  raliunxp  5017  resieq  5159  iss  5192  cnveqb  5329  funmo  5473  funimaexg  5533  fnbrfvb  5770  fvelimab  5785  fvmptss  5816  fmptco  5904  fprg  5918  fnressn  5921  fressnfv  5923  isoselem  6064  ovg  6215  caovcan  6254  caovordig  6255  caovord  6261  f1o2ndf1  6457  poxp  6461  fnse  6466  riotasvd  6595  riotasvdOLD  6596  smoeq  6615  smores  6617  smogt  6632  tfrlem1  6639  tfr3  6663  oaordi  6792  oeordi  6833  oeoa  6843  oeoe  6845  nnacl  6857  nnmcl  6858  nnecl  6859  nnacom  6863  nnaordi  6864  nnawordi  6867  nnaass  6868  nndi  6869  nnmass  6870  nnmsucr  6871  nnmcom  6872  nnmordi  6877  2ecoptocl  6998  3ecoptocl  6999  th3qlem2  7014  undifixp  7101  xpdom2g  7207  findcard2  7351  xpfi  7381  fnfi  7387  fodomfi  7388  finsschain  7416  marypha1lem  7441  marypha1  7442  supeq1  7453  ordiso2  7487  ordtypelem7  7496  wemaplem1  7518  inf3lem2  7587  inf3lem5  7590  infdiffi  7615  cantnfval2  7627  cantnfle  7629  cantnfp1lem3  7639  oemapval  7642  cantnflem1  7648  cantnf  7652  wemapwe  7657  cnfcom  7660  cnfcom3clem  7665  tz9.1  7668  r1pwOLD  7775  cplem2  7819  karden  7824  infxpenc2lem2  7906  fseqenlem1  7910  dfac8clem  7918  alephinit  7981  dfac4  8008  dfac5lem5  8013  dfac2a  8015  dfac2  8016  dfacacn  8026  dfac12lem3  8030  kmlem2  8036  kmlem13  8047  ackbij1lem16  8120  sornom  8162  infpssrlem4  8191  fin23lem14  8218  fin23lem32  8229  fin23lem34  8231  fin23lem36  8233  isf32lem1  8238  isf32lem2  8239  axcc2lem  8321  axcc3  8323  axcclem  8342  zornn0g  8390  ttukeylem5  8398  ttukeylem6  8399  axrepnd  8474  axpowndlem3  8479  zfcndrep  8494  fpwwe2lem8  8517  pwfseqlem3  8540  wunr1om  8599  wunfi  8601  tskr1om  8647  ingru  8695  grudomon  8697  axgroth3  8711  axgroth4  8712  nqereu  8811  mulcanenq  8842  elnp  8869  elnpi  8870  prlem934  8915  infm3  9972  nnaddcl  10027  nnmulcl  10028  peano5uzi  10363  uzind2  10367  uzindOLD  10369  zindd  10376  eluzadd  10519  uzaddcl  10538  uzwo  10544  uzwoOLD  10545  indstr  10550  zmax  10576  xmulasslem  10869  xrsupsslem  10890  xrinfmsslem  10891  xrsupss  10892  xrinfmss  10893  flval2  11226  om2uzlti  11295  uzrdgfni  11303  seqcl2  11346  seqfveq2  11350  seqshft2  11354  monoord  11358  seqsplit  11361  seqcaopr3  11363  seqf1olem2a  11366  seqf1o  11369  seqid2  11374  seqhomo  11375  ser1const  11384  expcllem  11397  expeq0  11415  mulexp  11424  expadd  11427  expmul  11430  leexp2r  11442  leexp1a  11443  bernneq  11510  modexp  11519  facdiv  11583  faclbnd  11586  faclbnd4lem4  11592  faclbnd6  11595  hashgadd  11656  hashxp  11702  hashmap  11703  hashf1lem2  11710  hashf1  11711  seqcoll  11717  wrdind  11796  cjexp  11960  absexp  12114  rlim  12294  rlim2  12295  rlim0  12307  rlim0lt  12308  rlimi  12312  ello12r  12316  ello1mpt  12320  ello1d  12322  elo12r  12327  lo1o1  12331  o1lo1  12336  lo1res  12358  climshft  12375  o1compt  12386  rlimo1  12415  lo1add  12425  lo1mul  12426  rlimdiv  12444  climub  12460  climserle  12461  caucvgrlem  12471  caurcvgr  12472  iseraltlem2  12481  summolem2a  12514  sumss  12523  fsum2d  12560  fsumabs  12585  fsumrlim  12595  fsumo1  12596  fsumiun  12605  binom  12614  bcxmas  12620  climcndslem1  12634  climcndslem2  12635  cvgrat  12665  demoivreALT  12807  ruclem8  12841  ruclem9  12842  dvdsle  12900  dvdsfac  12909  divalglem7  12924  bitsinv1  12959  sadcadd  12975  sadadd2  12977  saddisjlem  12981  smuval2  12999  smupvallem  13000  smu01lem  13002  smupval  13005  smueqlem  13007  smumullem  13009  bezoutlem4  13046  gcdmultiple  13055  rplpwr  13061  nn0seqcvgd  13066  seq1st  13067  alginv  13071  algcvga  13075  algfx  13076  prmind2  13095  prmdvdsexp  13119  prmfac1  13123  pcmpt  13266  pcfac  13273  prmpwdvds  13277  prmreclem4  13292  vdwlem10  13363  ramval  13381  ramcl  13402  prmlem1a  13434  imasleval  13771  ismre  13820  mreexexd  13878  lubprop  14442  lubid  14444  glbprop  14447  joinlem  14452  meetlem  14459  isglbd  14549  lubun  14555  oduclatb  14576  poslubmo  14578  poslubd  14579  spwmo  14663  spwpr4  14668  frmdgsum  14812  mulgnnass  14923  mhmmulg  14927  gsumwrev  15167  sylow1lem1  15237  efginvrel2  15364  efgsrel  15371  efgredlemd  15381  efgredlem  15384  efgred  15385  efgrelexlemb  15387  gsum2d  15551  gsumcom2  15554  ablfac1eulem  15635  pgpfac1lem2  15638  pgpfac1lem5  15642  pgpfac1  15643  pgpfac  15647  isdomn2  16364  mplcoe1  16533  mplcoe3  16534  mplcoe2  16535  cnfldexp  16739  fiinopn  16979  mretopd  17161  neiptoptop  17200  cnpfval  17303  iscnp3  17313  tgcn  17321  lmbr  17327  lmbr2  17328  lmbrf  17329  lmss  17367  ishaus  17391  hausnei2  17422  t1sep2  17438  fiuncmp  17472  dfcon2  17487  1stcfb  17513  2ndc1stc  17519  1stcrest  17521  1stcelcls  17529  1stccn  17531  lly1stc  17564  elkgen  17573  kgencn  17593  tx1stc  17687  xkopt  17692  cnmptcom  17715  isr0  17774  r0sep  17785  ptcmpfi  17850  isfildlem  17894  rnelfm  17990  fbflim  18013  flimrest  18020  isflf  18030  flffbas  18032  lmflf  18042  fclsrest  18061  isfcf  18071  cnextfvval  18101  tmdmulg  18127  tmdgsum  18130  eltsms  18167  tsmsi  18168  tsmsgsum  18173  tsmssubm  18177  tsmsres  18178  tsmsf1o  18179  isust  18238  isucn  18313  isucn2  18314  ucnima  18316  imasdsf1olem  18408  metss  18543  met1stc  18556  metcnp  18576  metcnpi  18579  metcnpi2  18580  metucnOLD  18623  metucn  18624  xrge0tsms  18870  fsumcn  18905  elcncf  18924  cncfi  18929  rescncf  18932  cncfco  18942  caucfil  19241  equivcau  19258  caubl  19265  caublcls  19266  ovolgelb  19381  ovolunlem1a  19397  ovolicc2lem3  19420  voliunlem1  19449  voliunlem3  19451  volsuplem  19454  volsup  19455  dyadmax  19495  vitali  19510  itg2leub  19629  itgfsum  19721  dvnadd  19820  dvnres  19822  cpnord  19826  dvnfre  19843  dvmptfsum  19864  dvferm1  19874  dvferm2  19876  rolle  19879  dvlip  19882  c1lip1  19886  lhop1  19903  deg1leb  20023  ply1divex  20064  fta1g  20095  plyco  20165  dgrcolem1  20196  dgrco  20198  dvnply2  20209  plydivex  20219  aalioulem2  20255  aalioulem3  20256  aalioulem5  20258  aaliou3lem2  20265  dvntaylp  20292  taylthlem1  20294  ulmdvlem3  20323  abelthlem9  20361  cxpmul2  20585  scvxcvx  20829  jensenlem2  20831  jensen  20832  wilthlem3  20858  perfectlem2  21019  bcmono  21066  bposlem5  21077  lgsquad2lem2  21148  dchrisumlem1  21188  dchrisum0flb  21209  pntpbnd1  21285  pntlemf  21304  qabvle  21324  qabvexp  21325  ostthlem2  21327  ostth2lem2  21333  sizeusglecusglem1  21498  2pthoncl  21608  fargshiftf1  21629  3v3e3cycl1  21636  4cycl4v4e  21658  4cycl4dv4e  21660  eupatrl  21695  eupath2  21707  isplig  21770  gxnn0add  21867  gxnn0mul  21870  ghgrp  21961  ghablo  21962  isnvlem  22094  nvi  22098  nmoubi  22278  nmounbi  22282  nmblolbi  22306  ipasslem1  22337  ipassi  22347  hlim2  22699  pjhth  22900  spansni  23064  elspansn2  23074  pjige0  23198  pjcjt2  23199  pjopyth  23227  elcnop  23365  elcnfn  23390  nmopub  23416  cnopc  23421  nmfnleub  23433  elnlfn  23436  cnfnc  23438  nmbdoplb  23533  nmcexi  23534  nmcoplb  23538  lnfnmul  23556  nmbdfnlb  23558  nmcfnlb  23562  pjss2coi  23672  pjssmi  23673  isst  23721  ishst  23722  stcltr1i  23782  mdbr  23802  dmdbr  23807  mddmd2  23817  mdslmd1lem3  23835  mdslmd1lem4  23836  elat2  23848  atcvat2  23897  cdj1i  23941  iuninc  24016  fmptcof2  24081  xrge0tsmsd  24228  isofld  24240  ofldadd  24243  ofldchr  24249  isarchi2  24260  esumfzf  24464  issiga  24499  isrnsiga  24501  ismeas  24558  isrnmeas  24559  measiun  24577  rrvsum  24717  subfacp1lem6  24876  erdszelem8  24889  isscon  24918  cvmliftlem7  24983  cvmliftlem10  24986  cvmlift3lem2  25012  ghomf1olem  25110  relexp0  25134  relexpsucr  25135  relexpsucl  25137  relexpind  25145  dfrtrclrec2  25148  rtrclreclem.refl  25149  rtrclreclem.subset  25150  rtrclreclem.min  25152  dfrtrcl2  25153  shftvalg  25213  clim2prod  25221  prodfn0  25227  prodfrec  25228  ntrivcvgfvn0  25232  prodmolem2a  25265  fprodabs  25302  fprodefsum  25303  fprodn0  25308  fprod2d  25310  iprodefisumlem  25322  binomfallfac  25362  faclimlem1  25367  dfpo2  25383  rdgprc  25427  preddowncl  25476  trpredmintr  25514  frmin  25522  soseq  25534  wfr3g  25542  wfrlem4  25546  frr3g  25586  bpolycl  26103  bpolydif  26106  fveleq  26206  heicant  26253  mbfresfi  26265  itg2gt0cn  26274  sdclem2  26460  fdc  26463  seqpo  26465  incsequz  26466  mettrifi  26477  prdsbnd2  26518  heiborlem4  26537  bfplem1  26545  iscringd  26623  maxidlval  26663  igenval2  26690  ismrc  26769  incssnn0  26779  mzpexpmpt  26816  pell14qrexpclnn0  26943  monotuz  27018  expmordi  27024  rmxypos  27026  jm2.17a  27039  jm2.17b  27040  rmygeid  27043  divalgmodcl  27072  jm2.18  27073  jm2.19lem3  27076  jm2.25  27084  jm2.15nn0  27088  jm2.16nn0  27089  wepwsolem  27130  aomclem8  27150  dfac11  27151  pwslnm  27187  islindf4  27299  lnr2i  27311  hbtlem5  27323  cnsrexpcl  27361  rngunsnply  27369  psgnunilem3  27410  isdomn3  27514  pm14.122b  27614  fnchoice  27690  fmul01  27700  fmuldfeq  27703  climsuselem1  27723  climinff  27727  stoweidlem2  27741  stoweidlem3  27742  stoweidlem17  27756  stoweidlem19  27758  stoweidlem21  27760  stoweidlem26  27765  2ffzoeq  28163  swrdccatin12lem4  28247  reumodprminv  28261  cshweqrep  28308  cshwssizesame  28322  usgra2pth  28349  wlkiswwlk2lem4  28376  wlkiswwlk2  28379  el2wlkonot  28401  el2spthonot  28402  frgra3vlem1  28464  3vfriswmgralem  28468  usg2spot2nb  28528  2spotmdisj  28531  bnj941  29217  bnj106  29313  bnj155  29324  bnj590  29355  bnj591  29356  bnj849  29370  bnj893  29373  bnj944  29383  bnj1128  29433  ax12olem6NEW7  29533  ax11v2NEW7  29604  ax15NEW7  29610  nfsb4twAUX7  29650  sbcomwAUX7  29662  sbcom2NEW7  29718  nfsb4tOLD7  29819  nfsb4tw2AUXOLD7  29820  sbcomOLD7  29829  lubunNEW  29845  isopos  30052  isat3  30179  ishlat1  30224  glbconN  30248  ispsubsp  30616  isldil  30981  isltrn  30990  isdilN  31025  trlval  31033  cdleme27b  31239  cdleme29b  31246  cdleme31sn1  31252  cdleme31sn1c  31259  cdleme40v  31340  cdlemk36  31784  cdlemkid5  31806  cdlemn11pre  32082  dihord2pre  32097  islpolN  32355  hdmapffval  32701  hdmapfval  32702  hdmapval2lem  32706
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