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

Theorem pm5.32da 624
Description: Distribution of implication over biconditional (deduction rule). (Contributed by NM, 9-Dec-2006.)
Hypothesis
Ref Expression
pm5.32da.1  |-  ( (
ph  /\  ps )  ->  ( ch  <->  th )
)
Assertion
Ref Expression
pm5.32da  |-  ( ph  ->  ( ( ps  /\  ch )  <->  ( ps  /\  th ) ) )

Proof of Theorem pm5.32da
StepHypRef Expression
1 pm5.32da.1 . . 3  |-  ( (
ph  /\  ps )  ->  ( ch  <->  th )
)
21ex 425 . 2  |-  ( ph  ->  ( ps  ->  ( ch 
<->  th ) ) )
32pm5.32d 622 1  |-  ( ph  ->  ( ( ps  /\  ch )  <->  ( ps  /\  th ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178    /\ wa 360
This theorem is referenced by:  rexbida  2726  reubida  2896  rmobida  2901  mpteq12f  4310  reuhypd  4779  funbrfv2b  5800  dffn5  5801  eqfnfv2  5857  fmptco  5930  dff13  6033  mpt2eq123dva  6164  mpt2eq3dva  6167  fnwelem  6490  mpt2xopovel  6500  opiota  6564  riotabidva  6595  oeeui  6874  omabs  6919  qliftfun  7018  erovlem  7029  xpcomco  7227  pw2f1olem  7241  elfi2  7448  cardval2  7909  dfac2  8042  cflim3  8173  iundom2g  8446  fpwwe2lem8  8543  fpwwe2lem12  8547  ltexpi  8810  ordpipq  8850  axrrecex  9069  nnunb  10248  zrevaddcl  10352  qrevaddcl  10627  icoshft  11050  fznn  11146  fznnfl  11274  fz1isolem  11741  2shfti  11926  limsupgle  12302  ello12  12341  elo12  12352  isercoll  12492  sumeq2ii  12518  fsum2dlem  12585  bitsmod  12979  bitscmp  12981  pwsle  13745  imasleval  13797  acsfiel  13910  ismon2  13991  isepi2  13998  oppcsect  14030  subsubc  14081  funcpropd  14128  fullpropd  14148  fucsect  14200  setcsect  14275  pltval3  14455  ismgmid  14741  grpidpropd  14753  mhmpropd  14775  issubm2  14780  subgacs  15006  eqgid  15023  pgpfi2  15271  eqgabl  15485  iscyggen2  15522  cyggenod  15525  eldprd  15593  subgdmdprd  15623  dprd2d2  15633  rngpropd  15726  crngunit  15798  dvdsrpropd  15832  drngpropd  15893  issubrg3  15927  lsslss  16068  lsspropd  16124  lmhmpropd  16176  lbspropd  16202  aspval2  16436  znleval  16866  znunithash  16876  pjdm2  16969  bastop2  17090  elcls2  17169  neiptopreu  17228  maxlp  17242  restopn2  17272  iscnp3  17339  subbascn  17349  lmbr2  17354  kgencn  17619  kgencn2  17620  hauseqlcld  17709  txlm  17711  txkgen  17715  xkoptsub  17717  idqtop  17769  tgqtop  17775  qtopcld  17776  elmptrab  17890  flimopn  18038  fbflim  18039  fbflim2  18040  flimrest  18046  flffbas  18058  flftg  18059  cnflf  18065  cnflf2  18066  txflf  18069  isfcls  18072  fclsopn  18077  fclsbas  18084  fclsrest  18087  fcfnei  18098  cnfcf  18105  ptcmplem2  18115  tgphaus  18177  tsmssubm  18203  isucn2  18340  ismet2  18394  xblpnfps  18456  xblpnf  18457  blin  18482  blres  18492  elmopn2  18506  imasf1obl  18549  imasf1oxms  18550  prdsbl  18552  neibl  18562  metrest  18585  metcnp3  18601  metcnp  18602  metcnp2  18603  metcn  18604  txmetcnp  18608  txmetcn  18609  metuel2  18640  metucnOLD  18649  metucn  18650  ngppropd  18709  cnbl0  18839  cnblcld  18840  bl2ioo  18854  xrtgioo  18868  elcncf2  18951  cncfmet  18969  nmhmcn  19159  lmmbr  19242  lmmbr2  19243  iscfil2  19250  iscau2  19261  iscau3  19262  lmclim  19286  shft2rab  19435  sca2rab  19439  mbfeqalem  19563  mbfmulc2lem  19568  mbfmax  19570  mbfposr  19573  mbfimaopnlem  19576  mbfaddlem  19581  mbfsup  19585  mbfinf  19586  i1fmullem  19615  i1fmulclem  19623  i1fres  19626  itg1climres  19635  mbfi1fseqlem4  19639  ibllem  19685  ellimc2  19795  ellimc3  19797  limcflf  19799  cnplimc  19805  cnlimc  19806  dvreslem  19827  ply1remlem  20116  fta1glem2  20120  ofmulrt  20230  plyremlem  20252  ulm2  20332  mcubic  20718  cubic2  20719  dvdsflsumcom  21004  fsumvma  21028  fsumvma2  21029  vmasum  21031  logfaclbnd  21037  dchrelbas2  21052  dchrelbas3  21053  dchrelbas4  21058  lgsquadlem1  21169  lgsquadlem2  21170  nbgrael  21469  nbcusgra  21503  eupath2  21733  isblo2  22315  ubthlem1  22403  h2hlm  22514  pjpreeq  22931  elnlfn  23462  reuxfr4d  24008  feqmptdf  24106  fmptcof2  24107  funcnvmpt  24114  gsumpropd2lem  24251  itgeq12dv  24672  orvcgteel  24756  prodeq2ii  25270  dfrdg2  25454  preduz  25506  predfz  25509  broutsideof3  26091  heicant  26277  cnambfre  26291  itg2gt0cn  26298  ftc1anclem5  26322  areacirclem5  26334  isfne4b  26388  filnetlem4  26448  isdrngo3  26613  isidlc  26663  prter3  26769  ellz1  26863  rmydioph  27123  rmxdioph  27125  expdiophlem1  27130  expdioph  27132  pw2f1ocnv  27146  dnwech  27161  islinds2  27298  sdrgacs  27524  pm14.123b  27641  rfcnpre1  27704  rfcnpre2  27716  rfcnpre3  27718  rfcnpre4  27719  climreeq  27753  funbrafv2b  28037  dfafn5a  28038  el2wlkonotot1  28430  usg2spthonot0  28445  islshpsm  29876  islshpat  29913  lkrsc  29993  lfl1dim  30017  ldual1dim  30062  isat3  30203  glbconxN  30273  islln2  30406  islpln2  30431  islvol2  30475  cdlemg2cex  31486  diaglbN  31951  diblsmopel  32067  dihopelvalcpre  32144  xihopellsmN  32150  dihopellsm  32151  dihglbcpreN  32196  mapdval4N  32528  hdmapoc  32830
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  df-an 362
  Copyright terms: Public domain W3C validator