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  1828  ax12olem6OLD  1970  ax11v2  2026  ax15  2054  nfsb4t  2113  sbcom  2122  ax11vALT  2130  sbcom2  2147  ax11eq  2227  ax11el  2228  ax11indalem  2231  ax11inda2ALT  2232  ax11inda  2234  ax11v2-o  2235  mo  2260  2mo  2316  2eu6  2323  2gencl  2928  3gencl  2929  vtocl2gf  2956  vtocl3gf  2957  eqeu  3048  mo2icl  3056  euind  3064  reu7  3072  reuind  3080  sbctt  3166  sbcnestgf  3241  r19.36zv  3671  dedth2h  3724  dedth3h  3725  dedth4h  3726  preq12bg  3919  elint  3998  elintrabg  4005  intab  4022  trss  4252  axrep1  4262  axrep2  4263  axrep3  4264  bm1.3ii  4274  pocl  4451  swopolem  4453  solin  4467  freq1  4493  frminex  4503  reusv3  4671  tfisi  4778  tfindsg  4780  tfinds2  4783  tfinds3  4784  dfom2  4787  elom  4788  findsg  4812  finds2  4813  vtoclr  4862  2optocl  4893  3optocl  4894  raliunxp  4954  resieq  5096  iss  5129  cnveqb  5266  funmo  5410  funimaexg  5470  fnbrfvb  5706  fvelimab  5721  fvmptss  5752  fmptco  5840  fprg  5854  fnressn  5857  fressnfv  5859  isoselem  6000  ovg  6151  caovcan  6190  caovordig  6191  caovord  6197  poxp  6394  fnse  6399  riotasvd  6528  riotasvdOLD  6529  smoeq  6548  smores  6550  smogt  6565  tfrlem1  6572  tfr3  6596  oaordi  6725  oeordi  6766  oeoa  6776  oeoe  6778  nnacl  6790  nnmcl  6791  nnecl  6792  nnacom  6796  nnaordi  6797  nnawordi  6800  nnaass  6801  nndi  6802  nnmass  6803  nnmsucr  6804  nnmcom  6805  nnmordi  6810  2ecoptocl  6931  3ecoptocl  6932  th3qlem2  6947  undifixp  7034  xpdom2g  7140  findcard2  7284  xpfi  7314  fnfi  7320  fodomfi  7321  finsschain  7348  marypha1lem  7373  marypha1  7374  supeq1  7385  ordiso2  7417  ordtypelem7  7426  wemaplem1  7448  inf3lem2  7517  inf3lem5  7520  infdiffi  7545  cantnfval2  7557  cantnfle  7559  cantnfp1lem3  7569  oemapval  7572  cantnflem1  7578  cantnf  7582  wemapwe  7587  cnfcom  7590  cnfcom3clem  7595  tz9.1  7598  r1pwOLD  7705  cplem2  7747  karden  7752  infxpenc2lem2  7834  fseqenlem1  7838  dfac8clem  7846  alephinit  7909  dfac4  7936  dfac5lem5  7941  dfac2a  7943  dfac2  7944  dfacacn  7954  dfac12lem3  7958  kmlem2  7964  kmlem13  7975  ackbij1lem16  8048  sornom  8090  infpssrlem4  8119  fin23lem14  8146  fin23lem32  8157  fin23lem34  8159  fin23lem36  8161  isf32lem1  8166  isf32lem2  8167  axcc2lem  8249  axcc3  8251  axcclem  8270  zornn0g  8318  ttukeylem5  8326  ttukeylem6  8327  axrepnd  8402  axpowndlem3  8407  zfcndrep  8422  fpwwe2lem8  8445  pwfseqlem3  8468  wunr1om  8527  wunfi  8529  tskr1om  8575  ingru  8623  grudomon  8625  axgroth3  8639  axgroth4  8640  nqereu  8739  mulcanenq  8770  elnp  8797  elnpi  8798  prlem934  8843  infm3  9899  nnaddcl  9954  nnmulcl  9955  peano5uzi  10290  uzind2  10294  uzindOLD  10296  zindd  10303  eluzadd  10446  uzaddcl  10465  uzwo  10471  uzwoOLD  10472  indstr  10477  zmax  10503  xmulasslem  10796  xrsupsslem  10817  xrinfmsslem  10818  xrsupss  10819  xrinfmss  10820  flval2  11148  om2uzlti  11217  uzrdgfni  11225  seqcl2  11268  seqfveq2  11272  seqshft2  11276  monoord  11280  seqsplit  11283  seqcaopr3  11285  seqf1olem2a  11288  seqf1o  11291  seqid2  11296  seqhomo  11297  ser1const  11306  expcllem  11319  expeq0  11337  mulexp  11346  expadd  11349  expmul  11352  leexp2r  11364  leexp1a  11365  bernneq  11432  modexp  11441  facdiv  11505  faclbnd  11508  faclbnd4lem4  11514  faclbnd6  11517  hashgadd  11578  hashxp  11624  hashmap  11625  hashf1lem2  11632  hashf1  11633  seqcoll  11639  wrdind  11718  cjexp  11882  absexp  12036  rlim  12216  rlim2  12217  rlim0  12229  rlim0lt  12230  rlimi  12234  ello12r  12238  ello1mpt  12242  ello1d  12244  elo12r  12249  lo1o1  12253  o1lo1  12258  lo1res  12280  climshft  12297  o1compt  12308  rlimo1  12337  lo1add  12347  lo1mul  12348  rlimdiv  12366  climub  12382  climserle  12383  caucvgrlem  12393  caurcvgr  12394  iseraltlem2  12403  summolem2a  12436  sumss  12445  fsum2d  12482  fsumabs  12507  fsumrlim  12517  fsumo1  12518  fsumiun  12527  binom  12536  bcxmas  12542  climcndslem1  12556  climcndslem2  12557  cvgrat  12587  demoivreALT  12729  ruclem8  12763  ruclem9  12764  dvdsle  12822  dvdsfac  12831  divalglem7  12846  bitsinv1  12881  sadcadd  12897  sadadd2  12899  saddisjlem  12903  smuval2  12921  smupvallem  12922  smu01lem  12924  smupval  12927  smueqlem  12929  smumullem  12931  bezoutlem4  12968  gcdmultiple  12977  rplpwr  12983  nn0seqcvgd  12988  seq1st  12989  alginv  12993  algcvga  12997  algfx  12998  prmind2  13017  prmdvdsexp  13041  prmfac1  13045  pcmpt  13188  pcfac  13195  prmpwdvds  13199  prmreclem4  13214  vdwlem10  13285  ramval  13303  ramcl  13324  prmlem1a  13356  imasleval  13693  ismre  13742  mreexexd  13800  lubprop  14364  lubid  14366  glbprop  14369  joinlem  14374  meetlem  14381  isglbd  14471  lubun  14477  oduclatb  14498  poslubmo  14500  poslubd  14501  spwmo  14585  spwpr4  14590  frmdgsum  14734  mulgnnass  14845  mhmmulg  14849  gsumwrev  15089  sylow1lem1  15159  efginvrel2  15286  efgsrel  15293  efgredlemd  15303  efgredlem  15306  efgred  15307  efgrelexlemb  15309  gsum2d  15473  gsumcom2  15476  ablfac1eulem  15557  pgpfac1lem2  15560  pgpfac1lem5  15564  pgpfac1  15565  pgpfac  15569  isdomn2  16286  mplcoe1  16455  mplcoe3  16456  mplcoe2  16457  cnfldexp  16657  fiinopn  16897  mretopd  17079  neiptoptop  17118  cnpfval  17220  iscnp3  17230  tgcn  17238  lmbr  17244  lmbr2  17245  lmbrf  17246  lmss  17284  ishaus  17308  hausnei2  17339  t1sep2  17355  fiuncmp  17389  dfcon2  17403  1stcfb  17429  2ndc1stc  17435  1stcrest  17437  1stcelcls  17445  1stccn  17447  lly1stc  17480  elkgen  17489  kgencn  17509  tx1stc  17603  xkopt  17608  cnmptcom  17631  isr0  17690  r0sep  17701  ptcmpfi  17766  isfildlem  17810  rnelfm  17906  fbflim  17929  flimrest  17936  isflf  17946  flffbas  17948  lmflf  17958  fclsrest  17977  isfcf  17987  cnextfvval  18017  tmdmulg  18043  tmdgsum  18046  eltsms  18083  tsmsi  18084  tsmsgsum  18089  tsmssubm  18093  tsmsres  18094  tsmsf1o  18095  isust  18154  isucn  18229  isucn2  18230  ucnima  18232  imasdsf1olem  18311  metss  18428  met1stc  18441  metcnp  18461  metcnpi  18464  metcnpi2  18465  metucn  18490  xrge0tsms  18736  fsumcn  18771  elcncf  18790  cncfi  18795  rescncf  18798  cncfco  18808  caucfil  19107  equivcau  19124  caubl  19131  caublcls  19132  ovolgelb  19243  ovolunlem1a  19259  ovolicc2lem3  19282  voliunlem1  19311  voliunlem3  19313  volsuplem  19316  volsup  19317  dyadmax  19357  vitali  19372  itg2leub  19493  itgfsum  19585  dvnadd  19682  dvnres  19684  cpnord  19688  dvnfre  19705  dvmptfsum  19726  dvferm1  19736  dvferm2  19738  rolle  19741  dvlip  19744  c1lip1  19748  lhop1  19765  deg1leb  19885  ply1divex  19926  fta1g  19957  plyco  20027  dgrcolem1  20058  dgrco  20060  dvnply2  20071  plydivex  20081  aalioulem2  20117  aalioulem3  20118  aalioulem5  20120  aaliou3lem2  20127  dvntaylp  20154  taylthlem1  20156  ulmdvlem3  20185  abelthlem9  20223  cxpmul2  20447  scvxcvx  20691  jensenlem2  20693  jensen  20694  wilthlem3  20720  perfectlem2  20881  bcmono  20928  bposlem5  20939  lgsquad2lem2  21010  dchrisumlem1  21050  dchrisum0flb  21071  pntpbnd1  21147  pntlemf  21166  qabvle  21186  qabvexp  21187  ostthlem2  21189  ostth2lem2  21195  nbusgra  21306  sizeusglecusglem1  21359  2pthoncl  21451  fargshiftf1  21472  3v3e3cycl1  21479  4cycl4v4e  21501  4cycl4dv4e  21503  eupatrl  21538  eupath2  21550  isplig  21613  gxnn0add  21710  gxnn0mul  21713  ghgrp  21804  ghablo  21805  isnvlem  21937  nvi  21941  nmoubi  22121  nmounbi  22125  nmblolbi  22149  ipasslem1  22180  ipassi  22190  hlim2  22542  pjhth  22743  spansni  22907  elspansn2  22917  pjige0  23041  pjcjt2  23042  pjopyth  23070  elcnop  23208  elcnfn  23233  nmopub  23259  cnopc  23264  nmfnleub  23276  elnlfn  23279  cnfnc  23281  nmbdoplb  23376  nmcexi  23377  nmcoplb  23381  lnfnmul  23399  nmbdfnlb  23401  nmcfnlb  23405  pjss2coi  23515  pjssmi  23516  isst  23564  ishst  23565  stcltr1i  23625  mdbr  23645  dmdbr  23650  mddmd2  23660  mdslmd1lem3  23678  mdslmd1lem4  23679  elat2  23691  atcvat2  23740  cdj1i  23784  iuninc  23855  fmptcof2  23918  xrge0tsmsd  24052  isofld  24061  ofldadd  24064  ofldchr  24070  esumfzf  24255  issiga  24290  isrnsiga  24292  ismeas  24349  isrnmeas  24350  measiun  24366  rrvsum  24491  subfacp1lem6  24650  erdszelem8  24663  isscon  24692  cvmliftlem7  24757  cvmliftlem10  24760  cvmlift3lem2  24786  ghomf1olem  24884  relexp0  24908  relexpsucr  24909  relexpsucl  24911  relexpind  24919  dfrtrclrec2  24922  rtrclreclem.refl  24923  rtrclreclem.subset  24924  rtrclreclem.min  24926  dfrtrcl2  24927  shftvalg  24987  clim2prod  24995  prodfn0  25001  prodfrec  25002  ntrivcvgfvn0  25006  prodmolem2a  25039  fprodabs  25076  fprodefsum  25077  fprodn0  25082  faclimlem1  25120  dfpo2  25136  rdgprc  25175  preddowncl  25220  trpredmintr  25258  frmin  25266  soseq  25278  wfr3g  25279  wfrlem4  25283  frr3g  25304  bpolycl  25812  bpolydif  25815  fveleq  25915  itg2gt0cn  25960  sdclem2  26137  fdc  26140  seqpo  26142  incsequz  26143  mettrifi  26154  prdsbnd2  26195  heiborlem4  26214  bfplem1  26222  iscringd  26300  maxidlval  26340  igenval2  26367  ismrc  26446  incssnn0  26456  mzpexpmpt  26493  pell14qrexpclnn0  26620  monotuz  26695  expmordi  26701  rmxypos  26703  jm2.17a  26716  jm2.17b  26717  rmygeid  26720  divalgmodcl  26749  jm2.18  26750  jm2.19lem3  26753  jm2.25  26761  jm2.15nn0  26765  jm2.16nn0  26766  wepwsolem  26807  aomclem8  26828  dfac11  26829  pwslnm  26865  islindf4  26977  lnr2i  26989  hbtlem5  27001  cnsrexpcl  27039  rngunsnply  27047  psgnunilem3  27088  isdomn3  27192  pm14.122b  27292  fnchoice  27368  fmul01  27378  fmuldfeq  27381  climsuselem1  27401  climinff  27405  stoweidlem2  27419  stoweidlem3  27420  stoweidlem17  27434  stoweidlem19  27436  stoweidlem21  27438  stoweidlem26  27443  frgra3vlem1  27753  3vfriswmgralem  27757  bnj941  28481  bnj106  28577  bnj155  28588  bnj590  28619  bnj591  28620  bnj849  28634  bnj893  28637  bnj944  28647  bnj1128  28697  ax12olem6NEW7  28797  ax11v2NEW7  28866  ax15NEW7  28872  nfsb4twAUX7  28912  sbcomwAUX7  28923  nfsb4tOLD7  29061  nfsb4tw2AUXOLD7  29062  sbcomOLD7  29071  sbcom2OLD7  29077  lubunNEW  29088  isopos  29295  isat3  29422  ishlat1  29467  glbconN  29491  ispsubsp  29859  isldil  30224  isltrn  30233  isdilN  30268  trlval  30276  cdleme27b  30482  cdleme29b  30489  cdleme31sn1  30495  cdleme31sn1c  30502  cdleme40v  30583  cdlemk36  31027  cdlemkid5  31049  cdlemn11pre  31325  dihord2pre  31340  islpolN  31598  hdmapffval  31944  hdmapfval  31945  hdmapval2lem  31949
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