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

Theorem pm5.32da 641
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 434 . 2  |-  ( ph  ->  ( ps  ->  ( ch 
<->  th ) ) )
32pm5.32d 639 1  |-  ( ph  ->  ( ( ps  /\  ch )  <->  ( ps  /\  th ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369
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 185  df-an 371
This theorem is referenced by:  rexbida  2947  rexbidva  2949  reubida  3024  rmobida  3029  mpteq12f  4510  reuhypd  4661  xpdifid  5422  funbrfv2b  5899  dffn5  5900  eqfnfv2  5964  fmptco  6046  dff13  6148  riotabidva  6256  mpt2eq123dva  6340  mpt2eq3dva  6343  opiota  6841  fnwelem  6897  suppssr  6930  mpt2xopovel  6947  mpt2curryd  6997  oeeui  7250  omabs  7295  qliftfun  7395  erovlem  7406  xpcomco  7606  pw2f1olem  7620  elfi2  7873  cardval2  8372  dfac2  8511  cflim3  8642  iundom2g  8915  fpwwe2lem8  9015  fpwwe2lem12  9019  ltexpi  9280  ordpipq  9320  axrrecex  9540  nnunb  10794  zrevaddcl  10912  qrevaddcl  11210  icoshft  11648  fznn  11753  fznnfl  11965  fz1isolem  12486  swrdeq  12647  wrdeqswrdlsw  12650  2swrdeqwrdeq  12654  2swrd1eqwrdeq  12655  2swrd2eqwrdeq  12867  2shfti  12889  limsupgle  13276  ello12  13315  elo12  13326  isercoll  13466  sumeq2ii  13491  fsum2dlem  13561  bitsmod  13960  bitscmp  13962  pwsle  14763  imasleval  14812  acsfiel  14925  ismon2  15003  isepi2  15010  oppcsect  15042  subsubc  15093  funcpropd  15140  fullpropd  15160  fucsect  15212  setcsect  15287  pltval3  15468  grpidpropd  15759  ismgmid  15762  gsumpropd2lem  15771  mhmpropd  15843  issubm2  15850  subgacs  16107  eqgid  16124  pgpfi2  16497  eqgabl  16714  iscyggen2  16755  cyggenod  16758  eldprd  16906  eldprdOLD  16908  subgdmdprd  16952  dprd2d2  16964  ringpropd  17101  crngunit  17182  dvdsrpropd  17216  drngpropd  17294  issubrg3  17328  lsslss  17478  lsspropd  17534  lmhmpropd  17590  lbspropd  17616  aspval2  17867  znleval  18463  znunithash  18473  pjdm2  18612  islinds2  18718  bastop2  19366  elcls2  19445  neiptopreu  19504  maxlp  19518  restopn2  19548  iscnp3  19615  subbascn  19625  lmbr2  19630  kgencn  19927  kgencn2  19928  hauseqlcld  20017  txlm  20019  txkgen  20023  xkoptsub  20025  idqtop  20077  tgqtop  20083  qtopcld  20084  elmptrab  20198  flimopn  20346  fbflim  20347  fbflim2  20348  flimrest  20354  flffbas  20366  flftg  20367  cnflf  20373  cnflf2  20374  txflf  20377  isfcls  20380  fclsopn  20385  fclsbas  20392  fclsrest  20395  fcfnei  20406  cnfcf  20413  ptcmplem2  20423  tgphaus  20485  tsmssubm  20514  isucn2  20652  ismet2  20706  xblpnfps  20768  xblpnf  20769  blin  20794  blres  20804  elmopn2  20818  imasf1obl  20861  imasf1oxms  20862  prdsbl  20864  neibl  20874  metrest  20897  metcnp3  20913  metcnp  20914  metcnp2  20915  metcn  20916  txmetcnp  20920  txmetcn  20921  metuel2  20952  metucnOLD  20961  metucn  20962  ngppropd  21021  cnbl0  21151  cnblcld  21152  bl2ioo  21167  xrtgioo  21181  elcncf2  21264  cncfmet  21282  nmhmcn  21473  lmmbr  21567  lmmbr2  21568  iscfil2  21575  iscau2  21586  iscau3  21587  lmclim  21611  shft2rab  21789  sca2rab  21793  mbfeqalem  21919  mbfmulc2lem  21924  mbfmax  21926  mbfposr  21929  mbfimaopnlem  21932  mbfaddlem  21937  mbfsup  21941  mbfinf  21942  i1fmullem  21971  i1fmulclem  21979  i1fres  21982  itg1climres  21991  mbfi1fseqlem4  21995  ibllem  22041  ellimc2  22151  ellimc3  22153  limcflf  22155  cnplimc  22161  cnlimc  22162  dvreslem  22183  ply1remlem  22433  fta1glem2  22437  ofmulrt  22547  plyremlem  22569  ulm2  22649  mcubic  23047  cubic2  23048  dvdsflsumcom  23333  fsumvma  23357  fsumvma2  23358  vmasum  23360  logfaclbnd  23366  dchrelbas2  23381  dchrelbas3  23382  dchrelbas4  23387  lgsquadlem1  23498  lgsquadlem2  23499  nbgrael  24295  nbcusgra  24332  clwwlkn2  24644  el2wlkonotot1  24743  usg2spthonot0  24758  eupath2  24849  isblo2  25567  ubthlem1  25655  h2hlm  25766  pjpreeq  26185  elnlfn  26716  reuxfr4d  27258  feqmptdf  27370  fmptcof2  27371  funcnvmpt  27379  fpwrelmapffslem  27424  nndiffz1  27465  ismntop  27874  itgeq12dv  28138  eulerpartlemgvv  28185  orvcgteel  28276  prodeq2ii  29017  dfrdg2  29200  preduz  29252  predfz  29255  broutsideof3  29748  heicant  30021  cnambfre  30035  itg2gt0cn  30042  ftc1anclem5  30066  areacirclem5  30083  isfne4b  30131  filnetlem4  30171  isdrngo3  30334  isidlc  30384  prter3  30595  ellz1  30672  rmydioph  30928  rmxdioph  30930  expdiophlem1  30935  expdioph  30937  pw2f1ocnv  30951  dnwech  30966  sdrgacs  31123  pm14.123b  31284  rfcnpre1  31345  rfcnpre2  31357  rfcnpre3  31359  rfcnpre4  31360  climreeq  31527  funbrafv2b  32082  dfafn5a  32083  mgmhmpropd  32311  issubmgm2  32316  isrnghmmul  32414  rngcsect  32525  rngcsectOLD  32537  ringcsect  32571  ringcsectOLD  32595  islshpsm  34428  islshpat  34465  lkrsc  34545  lfl1dim  34569  ldual1dim  34614  isat3  34755  glbconxN  34825  islln2  34958  islpln2  34983  islvol2  35027  cdlemg2cex  36040  diaglbN  36505  diblsmopel  36621  dihopelvalcpre  36698  xihopellsmN  36704  dihopellsm  36705  dihglbcpreN  36750  mapdval4N  37082  hdmapoc  37384
  Copyright terms: Public domain W3C validator