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

Theorem pm5.32da 622
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 423 . 2  |-  ( ph  ->  ( ps  ->  ( ch 
<->  th ) ) )
32pm5.32d 620 1  |-  ( ph  ->  ( ( ps  /\  ch )  <->  ( ps  /\  th ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358
This theorem is referenced by:  rexbida  2571  reubida  2735  rmobida  2740  mpteq12f  4112  reuhypd  4577  funbrfv2b  5583  dffn5  5584  eqfnfv2  5639  fmptco  5707  dff13  5799  mpt2eq123dva  5925  mpt2eq3dva  5928  fnwelem  6246  opiota  6306  riotabidva  6337  oeeui  6616  omabs  6661  qliftfun  6759  erovlem  6770  xpcomco  6968  pw2f1olem  6982  elfi2  7184  cardval2  7640  dfac2  7773  cflim3  7904  iundom2g  8178  fpwwe2lem8  8275  fpwwe2lem12  8279  ltexpi  8542  ordpipq  8582  axrrecex  8801  nnunb  9977  zrevaddcl  10079  qrevaddcl  10354  icoshft  10774  fznn  10868  fznnfl  10982  fz1isolem  11415  2shfti  11591  limsupgle  11967  ello12  12006  elo12  12017  isercoll  12157  sumeq2ii  12182  fsum2dlem  12249  bitsmod  12643  bitscmp  12645  pwsle  13407  imasleval  13459  acsfiel  13572  ismon2  13653  isepi2  13660  oppcsect  13692  subsubc  13743  funcpropd  13790  fullpropd  13810  fucsect  13862  setcsect  13937  pltval3  14117  ismgmid  14403  grpidpropd  14415  mhmpropd  14437  issubm2  14442  subgacs  14668  eqgid  14685  pgpfi2  14933  eqgabl  15147  iscyggen2  15184  cyggenod  15187  eldprd  15255  subgdmdprd  15285  dprd2d2  15295  rngpropd  15388  crngunit  15460  dvdsrpropd  15494  drngpropd  15555  issubrg3  15589  lsslss  15734  lsspropd  15790  lmhmpropd  15842  lbspropd  15868  aspval2  16102  znleval  16524  znunithash  16534  pjdm2  16627  bastop2  16748  elcls2  16827  maxlp  16894  restopn2  16924  iscnp3  16990  subbascn  17000  lmbr2  17005  kgencn  17267  kgencn2  17268  hauseqlcld  17356  txlm  17358  txkgen  17362  xkoptsub  17364  idqtop  17413  tgqtop  17419  qtopcld  17420  elmptrab  17538  flimopn  17686  fbflim  17687  fbflim2  17688  flimrest  17694  flffbas  17706  flftg  17707  cnflf  17713  cnflf2  17714  txflf  17717  isfcls  17720  fclsopn  17725  fclsbas  17732  fclsrest  17735  fcfnei  17746  cnfcf  17753  ptcmplem2  17763  tgphaus  17815  tsmssubm  17841  ismet2  17914  xblpnf  17969  blin  17986  blres  17993  elmopn2  18007  imasf1obl  18050  imasf1oxms  18051  prdsbl  18053  neibl  18063  metrest  18086  metcnp3  18102  metcnp  18103  metcnp2  18104  metcn  18105  txmetcnp  18109  txmetcn  18110  ngppropd  18169  cnbl0  18299  cnblcld  18300  bl2ioo  18314  xrtgioo  18328  elcncf2  18410  cncfmet  18428  nmhmcn  18617  lmmbr  18700  lmmbr2  18701  iscfil2  18708  iscau2  18719  iscau3  18720  lmclim  18744  shft2rab  18883  sca2rab  18887  mbfeqalem  19013  mbfmulc2lem  19018  mbfmax  19020  mbfposr  19023  mbfimaopnlem  19026  mbfaddlem  19031  mbfsup  19035  mbfinf  19036  i1fmullem  19065  i1fmulclem  19073  i1fres  19076  itg1climres  19085  mbfi1fseqlem4  19089  ibllem  19135  ellimc2  19243  ellimc3  19245  limcflf  19247  cnplimc  19253  cnlimc  19254  dvreslem  19275  ply1remlem  19564  fta1glem2  19568  ofmulrt  19678  plyremlem  19700  ulm2  19780  mcubic  20159  cubic2  20160  dvdsflsumcom  20444  fsumvma  20468  fsumvma2  20469  vmasum  20471  logfaclbnd  20477  dchrelbas2  20492  dchrelbas3  20493  dchrelbas4  20498  lgsquadlem1  20609  lgsquadlem2  20610  isblo2  21377  ubthlem1  21465  h2hlm  21576  pjpreeq  21993  elnlfn  22524  reuxfr4d  23155  itgeq12dv  23211  feqmptdf  23243  fmptcof2  23244  gsumpropd2lem  23394  orvcgteel  23683  eupath2  23919  cprodeq2ii  24135  dfrdg2  24223  preduz  24271  predfz  24274  broutsideof3  24821  itg2gt0cn  25006  areacirclem6  25033  surjsec2  25223  prodeq3ii  25411  svs2  25590  svs3  25591  isfne4b  26373  filnetlem4  26433  isdrngo3  26693  isidlc  26743  prter3  26853  ellz1  26949  rmydioph  27210  rmxdioph  27212  expdiophlem1  27217  expdioph  27219  pw2f1ocnv  27233  dnwech  27248  islinds2  27386  sdrgacs  27612  pm14.123b  27729  rfcnpre1  27793  rfcnpre2  27805  rfcnpre3  27807  rfcnpre4  27808  climreeq  27842  funbrafv2b  28127  dfafn5a  28128  mpt2xopovel  28202  nbgrael  28275  nbcusgra  28298  islshpsm  29792  islshpat  29829  lkrsc  29909  lfl1dim  29933  ldual1dim  29978  isat3  30119  glbconxN  30189  islln2  30322  islpln2  30347  islvol2  30391  cdlemg2cex  31402  diaglbN  31867  diblsmopel  31983  dihopelvalcpre  32060  xihopellsmN  32066  dihopellsm  32067  dihglbcpreN  32112  mapdval4N  32444  hdmapoc  32746
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 177  df-an 360
  Copyright terms: Public domain W3C validator