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

Theorem pm5.32da 645
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 435 . 2  |-  ( ph  ->  ( ps  ->  ( ch 
<->  th ) ) )
32pm5.32d 643 1  |-  ( ph  ->  ( ( ps  /\  ch )  <->  ( ps  /\  th ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    /\ wa 370
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 188  df-an 372
This theorem is referenced by:  rexbida  2931  rexbidva  2933  reubida  3008  rmobida  3013  mpteq12f  4500  reuhypd  4648  xpdifid  5284  funbrfv2b  5925  dffn5  5926  eqfnfv2  5992  fmptco  6071  dff13  6174  riotabidva  6283  mpt2eq123dva  6366  mpt2eq3dva  6369  opiota  6866  fnwelem  6922  suppssr  6957  mpt2xopovel  6977  mpt2curryd  7027  oeeui  7314  omabs  7359  qliftfun  7459  erovlem  7470  xpcomco  7671  pw2f1olem  7685  elfi2  7937  cardval2  8433  dfac2  8568  cflim3  8699  iundom2g  8972  fpwwe2lem8  9069  fpwwe2lem12  9073  ltexpi  9334  ordpipq  9374  axrrecex  9594  nnunb  10872  zrevaddcl  10989  qrevaddcl  11293  icoshft  11761  fznn  11870  preduz  11918  predfz  11921  fznnfl  12095  fz1isolem  12628  swrdeq  12802  2swrdeqwrdeq  12811  2swrd1eqwrdeq  12812  2swrd2eqwrdeq  13028  2shfti  13143  limsupgle  13534  ello12  13579  elo12  13590  isercoll  13730  sumeq2ii  13758  fsum2dlem  13830  prodeq2ii  13966  bitsmod  14409  bitscmp  14411  pwsle  15389  imasleval  15446  acsfiel  15559  ismon2  15638  isepi2  15645  oppcsect  15682  subsubc  15757  funcpropd  15804  fullpropd  15824  fucsect  15876  setcsect  15983  pltval3  16212  grpidpropd  16503  ismgmid  16506  gsumpropd2lem  16515  mhmpropd  16587  issubm2  16594  subgacs  16851  eqgid  16868  pgpfi2  17257  eqgabl  17474  iscyggen2  17515  cyggenod  17518  eldprd  17635  subgdmdprd  17666  dprd2d2  17676  ringpropd  17811  crngunit  17889  dvdsrpropd  17923  drngpropd  18001  issubrg3  18035  lsslss  18183  lsspropd  18239  lmhmpropd  18295  lbspropd  18321  aspval2  18570  znleval  19123  znunithash  19133  pjdm2  19272  islinds2  19369  bastop2  20008  elcls2  20088  neiptopreu  20147  maxlp  20161  restopn2  20191  iscnp3  20258  subbascn  20268  lmbr2  20273  kgencn  20569  kgencn2  20570  hauseqlcld  20659  txlm  20661  txkgen  20665  xkoptsub  20667  idqtop  20719  tgqtop  20725  qtopcld  20726  elmptrab  20840  flimopn  20988  fbflim  20989  fbflim2  20990  flimrest  20996  flffbas  21008  flftg  21009  cnflf  21015  cnflf2  21016  txflf  21019  isfcls  21022  fclsopn  21027  fclsbas  21034  fclsrest  21037  fcfnei  21048  cnfcf  21055  ptcmplem2  21066  tgphaus  21129  tsmssubm  21155  isucn2  21292  ismet2  21346  xblpnfps  21408  xblpnf  21409  blin  21434  blres  21444  elmopn2  21458  imasf1obl  21501  imasf1oxms  21502  prdsbl  21504  neibl  21514  metrest  21537  metcnp3  21553  metcnp  21554  metcnp2  21555  metcn  21556  txmetcnp  21560  txmetcn  21561  metuel2  21578  metucn  21584  ngppropd  21643  cnbl0  21792  cnblcld  21793  bl2ioo  21808  xrtgioo  21822  elcncf2  21920  cncfmet  21938  nmhmcn  22132  lmmbr  22226  lmmbr2  22227  iscfil2  22234  iscau2  22245  iscau3  22246  lmclim  22270  shft2rab  22459  sca2rab  22463  mbfeqalem  22596  mbfmulc2lem  22601  mbfmax  22603  mbfposr  22606  mbfimaopnlem  22609  mbfaddlem  22614  mbfsup  22618  mbfinf  22619  mbfinfOLD  22620  i1fmullem  22650  i1fmulclem  22658  i1fres  22661  itg1climres  22670  mbfi1fseqlem4  22674  ibllem  22720  ellimc2  22830  ellimc3  22832  limcflf  22834  cnplimc  22840  cnlimc  22841  dvreslem  22862  ply1remlem  23111  fta1glem2  23115  ofmulrt  23233  plyremlem  23255  ulm2  23338  mcubic  23771  cubic2  23772  dvdsflsumcom  24115  fsumvma  24139  fsumvma2  24140  vmasum  24142  logfaclbnd  24148  dchrelbas2  24163  dchrelbas3  24164  dchrelbas4  24169  lgsquadlem1  24280  lgsquadlem2  24281  colopp  24809  colhp  24810  nbgrael  25152  nbcusgra  25189  clwwlkn2  25501  el2wlkonotot1  25600  usg2spthonot0  25615  eupath2  25706  isblo2  26422  ubthlem1  26510  h2hlm  26631  pjpreeq  27049  elnlfn  27579  reuxfr4d  28124  feqmptdf  28260  fmptcof2  28261  funcnvmpt  28273  fpwrelmapffslem  28323  nndiffz1  28372  smatrcl  28630  ismntop  28838  itgeq12dv  29167  eulerpartlemgvv  29217  orvcgteel  29308  dfrdg2  30449  broutsideof3  30898  isfne4b  31002  filnetlem4  31042  poimirlem23  31927  poimirlem26  31930  poimirlem27  31931  heicant  31939  cnambfre  31953  itg2gt0cn  31961  ftc1anclem5  31985  areacirclem5  32000  isdrngo3  32162  isidlc  32212  prter3  32422  islshpsm  32515  islshpat  32552  lkrsc  32632  lfl1dim  32656  ldual1dim  32701  isat3  32842  glbconxN  32912  islln2  33045  islpln2  33070  islvol2  33114  cdlemg2cex  34127  diaglbN  34592  diblsmopel  34708  dihopelvalcpre  34785  xihopellsmN  34791  dihopellsm  34792  dihglbcpreN  34837  mapdval4N  35169  hdmapoc  35471  ellz1  35578  rmydioph  35839  rmxdioph  35841  expdiophlem1  35846  expdioph  35848  pw2f1ocnv  35862  dnwech  35876  sdrgacs  36037  pm14.123b  36747  rfcnpre1  37313  rfcnpre2  37325  rfcnpre3  37327  rfcnpre4  37328  climreeq  37633  funbrafv2b  38531  dfafn5a  38532  pfxeq  38815  pfxsuffeqwrdeq  38817  pfxsuff1eqwrdeq  38818  nbgrel  39177  mgmhmpropd  39405  issubmgm2  39410  isrnghmmul  39513  rngcsect  39602  rngcsectALTV  39614  ringcsect  39653  ringcsectALTV  39677  elbigo2  39985
  Copyright terms: Public domain W3C validator