MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  imbi2d Structured version   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  1838  ax12olem6OLD  2016  ax11v2  2074  ax11v2OLD  2075  ax15  2101  nfsb4tOLD  2155  sbcom  2164  ax11vALT  2172  sbcom2  2189  ax11eq  2269  ax11el  2270  ax11indalem  2273  ax11inda2ALT  2274  ax11inda  2276  ax11v2-o  2277  mo  2302  2mo  2358  2eu6  2365  2gencl  2977  3gencl  2978  vtocl2gf  3005  vtocl3gf  3006  eqeu  3097  mo2icl  3105  euind  3113  reu7  3121  reuind  3129  sbctt  3215  sbcnestgf  3290  r19.36zv  3720  dedth2h  3773  dedth3h  3774  dedth4h  3775  preq12bg  3969  elint  4048  elintrabg  4055  intab  4072  trss  4303  axrep1  4313  axrep2  4314  axrep3  4315  bm1.3ii  4325  pocl  4502  swopolem  4504  solin  4518  freq1  4544  frminex  4554  reusv3  4723  tfisi  4830  tfindsg  4832  tfinds2  4835  tfinds3  4836  dfom2  4839  elom  4840  findsg  4864  finds2  4865  vtoclr  4914  2optocl  4945  3optocl  4946  raliunxp  5006  resieq  5148  iss  5181  cnveqb  5318  funmo  5462  funimaexg  5522  fnbrfvb  5759  fvelimab  5774  fvmptss  5805  fmptco  5893  fprg  5907  fnressn  5910  fressnfv  5912  isoselem  6053  ovg  6204  caovcan  6243  caovordig  6244  caovord  6250  f1o2ndf1  6446  poxp  6450  fnse  6455  riotasvd  6584  riotasvdOLD  6585  smoeq  6604  smores  6606  smogt  6621  tfrlem1  6628  tfr3  6652  oaordi  6781  oeordi  6822  oeoa  6832  oeoe  6834  nnacl  6846  nnmcl  6847  nnecl  6848  nnacom  6852  nnaordi  6853  nnawordi  6856  nnaass  6857  nndi  6858  nnmass  6859  nnmsucr  6860  nnmcom  6861  nnmordi  6866  2ecoptocl  6987  3ecoptocl  6988  th3qlem2  7003  undifixp  7090  xpdom2g  7196  findcard2  7340  xpfi  7370  fnfi  7376  fodomfi  7377  finsschain  7405  marypha1lem  7430  marypha1  7431  supeq1  7442  ordiso2  7476  ordtypelem7  7485  wemaplem1  7507  inf3lem2  7576  inf3lem5  7579  infdiffi  7604  cantnfval2  7616  cantnfle  7618  cantnfp1lem3  7628  oemapval  7631  cantnflem1  7637  cantnf  7641  wemapwe  7646  cnfcom  7649  cnfcom3clem  7654  tz9.1  7657  r1pwOLD  7764  cplem2  7806  karden  7811  infxpenc2lem2  7893  fseqenlem1  7897  dfac8clem  7905  alephinit  7968  dfac4  7995  dfac5lem5  8000  dfac2a  8002  dfac2  8003  dfacacn  8013  dfac12lem3  8017  kmlem2  8023  kmlem13  8034  ackbij1lem16  8107  sornom  8149  infpssrlem4  8178  fin23lem14  8205  fin23lem32  8216  fin23lem34  8218  fin23lem36  8220  isf32lem1  8225  isf32lem2  8226  axcc2lem  8308  axcc3  8310  axcclem  8329  zornn0g  8377  ttukeylem5  8385  ttukeylem6  8386  axrepnd  8461  axpowndlem3  8466  zfcndrep  8481  fpwwe2lem8  8504  pwfseqlem3  8527  wunr1om  8586  wunfi  8588  tskr1om  8634  ingru  8682  grudomon  8684  axgroth3  8698  axgroth4  8699  nqereu  8798  mulcanenq  8829  elnp  8856  elnpi  8857  prlem934  8902  infm3  9959  nnaddcl  10014  nnmulcl  10015  peano5uzi  10350  uzind2  10354  uzindOLD  10356  zindd  10363  eluzadd  10506  uzaddcl  10525  uzwo  10531  uzwoOLD  10532  indstr  10537  zmax  10563  xmulasslem  10856  xrsupsslem  10877  xrinfmsslem  10878  xrsupss  10879  xrinfmss  10880  flval2  11213  om2uzlti  11282  uzrdgfni  11290  seqcl2  11333  seqfveq2  11337  seqshft2  11341  monoord  11345  seqsplit  11348  seqcaopr3  11350  seqf1olem2a  11353  seqf1o  11356  seqid2  11361  seqhomo  11362  ser1const  11371  expcllem  11384  expeq0  11402  mulexp  11411  expadd  11414  expmul  11417  leexp2r  11429  leexp1a  11430  bernneq  11497  modexp  11506  facdiv  11570  faclbnd  11573  faclbnd4lem4  11579  faclbnd6  11582  hashgadd  11643  hashxp  11689  hashmap  11690  hashf1lem2  11697  hashf1  11698  seqcoll  11704  wrdind  11783  cjexp  11947  absexp  12101  rlim  12281  rlim2  12282  rlim0  12294  rlim0lt  12295  rlimi  12299  ello12r  12303  ello1mpt  12307  ello1d  12309  elo12r  12314  lo1o1  12318  o1lo1  12323  lo1res  12345  climshft  12362  o1compt  12373  rlimo1  12402  lo1add  12412  lo1mul  12413  rlimdiv  12431  climub  12447  climserle  12448  caucvgrlem  12458  caurcvgr  12459  iseraltlem2  12468  summolem2a  12501  sumss  12510  fsum2d  12547  fsumabs  12572  fsumrlim  12582  fsumo1  12583  fsumiun  12592  binom  12601  bcxmas  12607  climcndslem1  12621  climcndslem2  12622  cvgrat  12652  demoivreALT  12794  ruclem8  12828  ruclem9  12829  dvdsle  12887  dvdsfac  12896  divalglem7  12911  bitsinv1  12946  sadcadd  12962  sadadd2  12964  saddisjlem  12968  smuval2  12986  smupvallem  12987  smu01lem  12989  smupval  12992  smueqlem  12994  smumullem  12996  bezoutlem4  13033  gcdmultiple  13042  rplpwr  13048  nn0seqcvgd  13053  seq1st  13054  alginv  13058  algcvga  13062  algfx  13063  prmind2  13082  prmdvdsexp  13106  prmfac1  13110  pcmpt  13253  pcfac  13260  prmpwdvds  13264  prmreclem4  13279  vdwlem10  13350  ramval  13368  ramcl  13389  prmlem1a  13421  imasleval  13758  ismre  13807  mreexexd  13865  lubprop  14429  lubid  14431  glbprop  14434  joinlem  14439  meetlem  14446  isglbd  14536  lubun  14542  oduclatb  14563  poslubmo  14565  poslubd  14566  spwmo  14650  spwpr4  14655  frmdgsum  14799  mulgnnass  14910  mhmmulg  14914  gsumwrev  15154  sylow1lem1  15224  efginvrel2  15351  efgsrel  15358  efgredlemd  15368  efgredlem  15371  efgred  15372  efgrelexlemb  15374  gsum2d  15538  gsumcom2  15541  ablfac1eulem  15622  pgpfac1lem2  15625  pgpfac1lem5  15629  pgpfac1  15630  pgpfac  15634  isdomn2  16351  mplcoe1  16520  mplcoe3  16521  mplcoe2  16522  cnfldexp  16726  fiinopn  16966  mretopd  17148  neiptoptop  17187  cnpfval  17290  iscnp3  17300  tgcn  17308  lmbr  17314  lmbr2  17315  lmbrf  17316  lmss  17354  ishaus  17378  hausnei2  17409  t1sep2  17425  fiuncmp  17459  dfcon2  17474  1stcfb  17500  2ndc1stc  17506  1stcrest  17508  1stcelcls  17516  1stccn  17518  lly1stc  17551  elkgen  17560  kgencn  17580  tx1stc  17674  xkopt  17679  cnmptcom  17702  isr0  17761  r0sep  17772  ptcmpfi  17837  isfildlem  17881  rnelfm  17977  fbflim  18000  flimrest  18007  isflf  18017  flffbas  18019  lmflf  18029  fclsrest  18048  isfcf  18058  cnextfvval  18088  tmdmulg  18114  tmdgsum  18117  eltsms  18154  tsmsi  18155  tsmsgsum  18160  tsmssubm  18164  tsmsres  18165  tsmsf1o  18166  isust  18225  isucn  18300  isucn2  18301  ucnima  18303  imasdsf1olem  18395  metss  18530  met1stc  18543  metcnp  18563  metcnpi  18566  metcnpi2  18567  metucnOLD  18610  metucn  18611  xrge0tsms  18857  fsumcn  18892  elcncf  18911  cncfi  18916  rescncf  18919  cncfco  18929  caucfil  19228  equivcau  19245  caubl  19252  caublcls  19253  ovolgelb  19368  ovolunlem1a  19384  ovolicc2lem3  19407  voliunlem1  19436  voliunlem3  19438  volsuplem  19441  volsup  19442  dyadmax  19482  vitali  19497  itg2leub  19618  itgfsum  19710  dvnadd  19807  dvnres  19809  cpnord  19813  dvnfre  19830  dvmptfsum  19851  dvferm1  19861  dvferm2  19863  rolle  19866  dvlip  19869  c1lip1  19873  lhop1  19890  deg1leb  20010  ply1divex  20051  fta1g  20082  plyco  20152  dgrcolem1  20183  dgrco  20185  dvnply2  20196  plydivex  20206  aalioulem2  20242  aalioulem3  20243  aalioulem5  20245  aaliou3lem2  20252  dvntaylp  20279  taylthlem1  20281  ulmdvlem3  20310  abelthlem9  20348  cxpmul2  20572  scvxcvx  20816  jensenlem2  20818  jensen  20819  wilthlem3  20845  perfectlem2  21006  bcmono  21053  bposlem5  21064  lgsquad2lem2  21135  dchrisumlem1  21175  dchrisum0flb  21196  pntpbnd1  21272  pntlemf  21291  qabvle  21311  qabvexp  21312  ostthlem2  21314  ostth2lem2  21320  sizeusglecusglem1  21485  2pthoncl  21595  fargshiftf1  21616  3v3e3cycl1  21623  4cycl4v4e  21645  4cycl4dv4e  21647  eupatrl  21682  eupath2  21694  isplig  21757  gxnn0add  21854  gxnn0mul  21857  ghgrp  21948  ghablo  21949  isnvlem  22081  nvi  22085  nmoubi  22265  nmounbi  22269  nmblolbi  22293  ipasslem1  22324  ipassi  22334  hlim2  22686  pjhth  22887  spansni  23051  elspansn2  23061  pjige0  23185  pjcjt2  23186  pjopyth  23214  elcnop  23352  elcnfn  23377  nmopub  23403  cnopc  23408  nmfnleub  23420  elnlfn  23423  cnfnc  23425  nmbdoplb  23520  nmcexi  23521  nmcoplb  23525  lnfnmul  23543  nmbdfnlb  23545  nmcfnlb  23549  pjss2coi  23659  pjssmi  23660  isst  23708  ishst  23709  stcltr1i  23769  mdbr  23789  dmdbr  23794  mddmd2  23804  mdslmd1lem3  23822  mdslmd1lem4  23823  elat2  23835  atcvat2  23884  cdj1i  23928  iuninc  24003  fmptcof2  24068  xrge0tsmsd  24215  isofld  24227  ofldadd  24230  ofldchr  24236  isarchi2  24247  esumfzf  24451  issiga  24486  isrnsiga  24488  ismeas  24545  isrnmeas  24546  measiun  24564  rrvsum  24704  subfacp1lem6  24863  erdszelem8  24876  isscon  24905  cvmliftlem7  24970  cvmliftlem10  24973  cvmlift3lem2  24999  ghomf1olem  25097  relexp0  25121  relexpsucr  25122  relexpsucl  25124  relexpind  25132  dfrtrclrec2  25135  rtrclreclem.refl  25136  rtrclreclem.subset  25137  rtrclreclem.min  25139  dfrtrcl2  25140  shftvalg  25200  clim2prod  25208  prodfn0  25214  prodfrec  25215  ntrivcvgfvn0  25219  prodmolem2a  25252  fprodabs  25289  fprodefsum  25290  fprodn0  25295  fprod2d  25297  iprodefisumlem  25309  binomfallfac  25349  faclimlem1  25354  dfpo2  25370  rdgprc  25414  preddowncl  25463  trpredmintr  25501  frmin  25509  soseq  25521  wfr3g  25529  wfrlem4  25533  frr3g  25573  bpolycl  26090  bpolydif  26093  fveleq  26193  mbfresfi  26243  itg2gt0cn  26250  sdclem2  26437  fdc  26440  seqpo  26442  incsequz  26443  mettrifi  26454  prdsbnd2  26495  heiborlem4  26514  bfplem1  26522  iscringd  26600  maxidlval  26640  igenval2  26667  ismrc  26746  incssnn0  26756  mzpexpmpt  26793  pell14qrexpclnn0  26920  monotuz  26995  expmordi  27001  rmxypos  27003  jm2.17a  27016  jm2.17b  27017  rmygeid  27020  divalgmodcl  27049  jm2.18  27050  jm2.19lem3  27053  jm2.25  27061  jm2.15nn0  27065  jm2.16nn0  27066  wepwsolem  27107  aomclem8  27127  dfac11  27128  pwslnm  27164  islindf4  27276  lnr2i  27288  hbtlem5  27300  cnsrexpcl  27338  rngunsnply  27346  psgnunilem3  27387  isdomn3  27491  pm14.122b  27591  fnchoice  27667  fmul01  27677  fmuldfeq  27680  climsuselem1  27700  climinff  27704  stoweidlem2  27718  stoweidlem3  27719  stoweidlem17  27733  stoweidlem19  27735  stoweidlem21  27737  stoweidlem26  27742  swrdccatin12lem4  28179  reumodprminv  28193  cshweqrep  28237  cshwssizesame  28251  usgra2pth  28264  el2wlkonot  28289  el2spthonot  28290  frgra3vlem1  28327  3vfriswmgralem  28331  usg2spot2nb  28391  2spotmdisj  28394  bnj941  29080  bnj106  29176  bnj155  29187  bnj590  29218  bnj591  29219  bnj849  29233  bnj893  29236  bnj944  29246  bnj1128  29296  ax12olem6NEW7  29396  ax11v2NEW7  29467  ax15NEW7  29473  nfsb4twAUX7  29513  sbcomwAUX7  29525  sbcom2NEW7  29581  nfsb4tOLD7  29682  nfsb4tw2AUXOLD7  29683  sbcomOLD7  29692  lubunNEW  29708  isopos  29915  isat3  30042  ishlat1  30087  glbconN  30111  ispsubsp  30479  isldil  30844  isltrn  30853  isdilN  30888  trlval  30896  cdleme27b  31102  cdleme29b  31109  cdleme31sn1  31115  cdleme31sn1c  31122  cdleme40v  31203  cdlemk36  31647  cdlemkid5  31669  cdlemn11pre  31945  dihord2pre  31960  islpolN  32218  hdmapffval  32564  hdmapfval  32565  hdmapval2lem  32569
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