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

Theorem pm5.32da 634
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 632 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  2720  reubida  2893  rmobida  2898  mpteq12f  4356  reuhypd  4507  xpdifid  5254  funbrfv2b  5724  dffn5  5725  eqfnfv2  5786  fmptco  5863  dff13  5958  riotabidva  6057  mpt2eq123dva  6136  mpt2eq3dva  6139  opiota  6622  fnwelem  6676  suppssr  6709  mpt2xopovel  6726  oeeui  7029  omabs  7074  qliftfun  7173  erovlem  7184  xpcomco  7389  pw2f1olem  7403  elfi2  7652  cardval2  8149  dfac2  8288  cflim3  8419  iundom2g  8692  fpwwe2lem8  8792  fpwwe2lem12  8796  ltexpi  9059  ordpipq  9099  axrrecex  9318  nnunb  10563  zrevaddcl  10678  qrevaddcl  10963  icoshft  11394  fznn  11510  fznnfl  11685  fz1isolem  12198  swrdeq  12324  wrdeqswrdlsw  12327  2swrdeqwrdeq  12331  2swrd1eqwrdeq  12332  2swrd2eqwrdeq  12537  2shfti  12553  limsupgle  12939  ello12  12978  elo12  12989  isercoll  13129  sumeq2ii  13154  fsum2dlem  13221  bitsmod  13615  bitscmp  13617  pwsle  14413  imasleval  14462  acsfiel  14575  ismon2  14656  isepi2  14663  oppcsect  14695  subsubc  14746  funcpropd  14793  fullpropd  14813  fucsect  14865  setcsect  14940  pltval3  15120  ismgmid  15418  grpidpropd  15430  mhmpropd  15453  issubm2  15458  subgacs  15696  eqgid  15713  pgpfi2  16085  eqgabl  16299  iscyggen2  16338  cyggenod  16341  eldprd  16460  eldprdOLD  16462  subgdmdprd  16505  dprd2d2  16517  rngpropd  16612  crngunit  16688  dvdsrpropd  16722  drngpropd  16783  issubrg3  16817  lsslss  16964  lsspropd  17020  lmhmpropd  17076  lbspropd  17102  aspval2  17339  znleval  17829  znunithash  17839  pjdm2  17978  islinds2  18084  bastop2  18441  elcls2  18520  neiptopreu  18579  maxlp  18593  restopn2  18623  iscnp3  18690  subbascn  18700  lmbr2  18705  kgencn  18971  kgencn2  18972  hauseqlcld  19061  txlm  19063  txkgen  19067  xkoptsub  19069  idqtop  19121  tgqtop  19127  qtopcld  19128  elmptrab  19242  flimopn  19390  fbflim  19391  fbflim2  19392  flimrest  19398  flffbas  19410  flftg  19411  cnflf  19417  cnflf2  19418  txflf  19421  isfcls  19424  fclsopn  19429  fclsbas  19436  fclsrest  19439  fcfnei  19450  cnfcf  19457  ptcmplem2  19467  tgphaus  19529  tsmssubm  19558  isucn2  19696  ismet2  19750  xblpnfps  19812  xblpnf  19813  blin  19838  blres  19848  elmopn2  19862  imasf1obl  19905  imasf1oxms  19906  prdsbl  19908  neibl  19918  metrest  19941  metcnp3  19957  metcnp  19958  metcnp2  19959  metcn  19960  txmetcnp  19964  txmetcn  19965  metuel2  19996  metucnOLD  20005  metucn  20006  ngppropd  20065  cnbl0  20195  cnblcld  20196  bl2ioo  20211  xrtgioo  20225  elcncf2  20308  cncfmet  20326  nmhmcn  20517  lmmbr  20611  lmmbr2  20612  iscfil2  20619  iscau2  20630  iscau3  20631  lmclim  20655  shft2rab  20833  sca2rab  20837  mbfeqalem  20962  mbfmulc2lem  20967  mbfmax  20969  mbfposr  20972  mbfimaopnlem  20975  mbfaddlem  20980  mbfsup  20984  mbfinf  20985  i1fmullem  21014  i1fmulclem  21022  i1fres  21025  itg1climres  21034  mbfi1fseqlem4  21038  ibllem  21084  ellimc2  21194  ellimc3  21196  limcflf  21198  cnplimc  21204  cnlimc  21205  dvreslem  21226  ply1remlem  21519  fta1glem2  21523  ofmulrt  21633  plyremlem  21655  ulm2  21735  mcubic  22127  cubic2  22128  dvdsflsumcom  22413  fsumvma  22437  fsumvma2  22438  vmasum  22440  logfaclbnd  22446  dchrelbas2  22461  dchrelbas3  22462  dchrelbas4  22467  lgsquadlem1  22578  lgsquadlem2  22579  nbgrael  23160  nbcusgra  23194  eupath2  23424  isblo2  24006  ubthlem1  24094  h2hlm  24205  pjpreeq  24624  elnlfn  25155  reuxfr4d  25698  feqmptdf  25802  fmptcof2  25803  funcnvmpt  25811  fpwrelmapffslem  25857  nndiffz1  25898  gsumpropd2lem  26093  itgeq12dv  26560  eulerpartlemgvv  26607  orvcgteel  26698  prodeq2ii  27273  dfrdg2  27456  preduz  27508  predfz  27511  broutsideof3  28004  heicant  28270  cnambfre  28284  itg2gt0cn  28291  ftc1anclem5  28315  areacirclem5  28332  isfne4b  28386  filnetlem4  28446  isdrngo3  28609  isidlc  28659  prter3  28872  ellz1  28950  rmydioph  29208  rmxdioph  29210  expdiophlem1  29215  expdioph  29217  pw2f1ocnv  29231  dnwech  29246  sdrgacs  29403  pm14.123b  29525  rfcnpre1  29586  rfcnpre2  29598  rfcnpre3  29600  rfcnpre4  29601  climreeq  29632  funbrafv2b  29911  dfafn5a  29912  el2wlkonotot1  30239  usg2spthonot0  30254  clwwlkn2  30284  islshpsm  32219  islshpat  32256  lkrsc  32336  lfl1dim  32360  ldual1dim  32405  isat3  32546  glbconxN  32616  islln2  32749  islpln2  32774  islvol2  32818  cdlemg2cex  33829  diaglbN  34294  diblsmopel  34410  dihopelvalcpre  34487  xihopellsmN  34493  dihopellsm  34494  dihglbcpreN  34539  mapdval4N  34871  hdmapoc  35173
  Copyright terms: Public domain W3C validator