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

Theorem pm5.32da 623
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 424 . 2  |-  ( ph  ->  ( ps  ->  ( ch 
<->  th ) ) )
32pm5.32d 621 1  |-  ( ph  ->  ( ( ps  /\  ch )  <->  ( ps  /\  th ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359
This theorem is referenced by:  rexbida  2712  reubida  2882  rmobida  2887  mpteq12f  4277  reuhypd  4741  funbrfv2b  5762  dffn5  5763  eqfnfv2  5819  fmptco  5892  dff13  5995  mpt2eq123dva  6126  mpt2eq3dva  6129  fnwelem  6452  mpt2xopovel  6462  opiota  6526  riotabidva  6557  oeeui  6836  omabs  6881  qliftfun  6980  erovlem  6991  xpcomco  7189  pw2f1olem  7203  elfi2  7410  cardval2  7867  dfac2  8000  cflim3  8131  iundom2g  8404  fpwwe2lem8  8501  fpwwe2lem12  8505  ltexpi  8768  ordpipq  8808  axrrecex  9027  nnunb  10206  zrevaddcl  10310  qrevaddcl  10585  icoshft  11008  fznn  11103  fznnfl  11231  fz1isolem  11698  2shfti  11883  limsupgle  12259  ello12  12298  elo12  12309  isercoll  12449  sumeq2ii  12475  fsum2dlem  12542  bitsmod  12936  bitscmp  12938  pwsle  13702  imasleval  13754  acsfiel  13867  ismon2  13948  isepi2  13955  oppcsect  13987  subsubc  14038  funcpropd  14085  fullpropd  14105  fucsect  14157  setcsect  14232  pltval3  14412  ismgmid  14698  grpidpropd  14710  mhmpropd  14732  issubm2  14737  subgacs  14963  eqgid  14980  pgpfi2  15228  eqgabl  15442  iscyggen2  15479  cyggenod  15482  eldprd  15550  subgdmdprd  15580  dprd2d2  15590  rngpropd  15683  crngunit  15755  dvdsrpropd  15789  drngpropd  15850  issubrg3  15884  lsslss  16025  lsspropd  16081  lmhmpropd  16133  lbspropd  16159  aspval2  16393  znleval  16823  znunithash  16833  pjdm2  16926  bastop2  17047  elcls2  17126  neiptopreu  17185  maxlp  17199  restopn2  17229  iscnp3  17296  subbascn  17306  lmbr2  17311  kgencn  17576  kgencn2  17577  hauseqlcld  17666  txlm  17668  txkgen  17672  xkoptsub  17674  idqtop  17726  tgqtop  17732  qtopcld  17733  elmptrab  17847  flimopn  17995  fbflim  17996  fbflim2  17997  flimrest  18003  flffbas  18015  flftg  18016  cnflf  18022  cnflf2  18023  txflf  18026  isfcls  18029  fclsopn  18034  fclsbas  18041  fclsrest  18044  fcfnei  18055  cnfcf  18062  ptcmplem2  18072  tgphaus  18134  tsmssubm  18160  isucn2  18297  ismet2  18351  xblpnfps  18413  xblpnf  18414  blin  18439  blres  18449  elmopn2  18463  imasf1obl  18506  imasf1oxms  18507  prdsbl  18509  neibl  18519  metrest  18542  metcnp3  18558  metcnp  18559  metcnp2  18560  metcn  18561  txmetcnp  18565  txmetcn  18566  metuel2  18597  metucnOLD  18606  metucn  18607  ngppropd  18666  cnbl0  18796  cnblcld  18797  bl2ioo  18811  xrtgioo  18825  elcncf2  18908  cncfmet  18926  nmhmcn  19116  lmmbr  19199  lmmbr2  19200  iscfil2  19207  iscau2  19218  iscau3  19219  lmclim  19243  shft2rab  19392  sca2rab  19396  mbfeqalem  19522  mbfmulc2lem  19527  mbfmax  19529  mbfposr  19532  mbfimaopnlem  19535  mbfaddlem  19540  mbfsup  19544  mbfinf  19545  i1fmullem  19574  i1fmulclem  19582  i1fres  19585  itg1climres  19594  mbfi1fseqlem4  19598  ibllem  19644  ellimc2  19752  ellimc3  19754  limcflf  19756  cnplimc  19762  cnlimc  19763  dvreslem  19784  ply1remlem  20073  fta1glem2  20077  ofmulrt  20187  plyremlem  20209  ulm2  20289  mcubic  20675  cubic2  20676  dvdsflsumcom  20961  fsumvma  20985  fsumvma2  20986  vmasum  20988  logfaclbnd  20994  dchrelbas2  21009  dchrelbas3  21010  dchrelbas4  21015  lgsquadlem1  21126  lgsquadlem2  21127  nbgrael  21426  nbcusgra  21460  eupath2  21690  isblo2  22272  ubthlem1  22360  h2hlm  22471  pjpreeq  22888  elnlfn  23419  reuxfr4d  23965  feqmptdf  24063  fmptcof2  24064  funcnvmpt  24071  gsumpropd2lem  24208  itgeq12dv  24629  orvcgteel  24713  prodeq2ii  25228  dfrdg2  25407  preduz  25455  predfz  25458  broutsideof3  26008  cnambfre  26201  itg2gt0cn  26206  areacirclem6  26233  isfne4b  26287  filnetlem4  26347  isdrngo3  26512  isidlc  26562  prter3  26668  ellz1  26762  rmydioph  27022  rmxdioph  27024  expdiophlem1  27029  expdioph  27031  pw2f1ocnv  27045  dnwech  27060  islinds2  27198  sdrgacs  27424  pm14.123b  27541  rfcnpre1  27604  rfcnpre2  27616  rfcnpre3  27618  rfcnpre4  27619  climreeq  27653  funbrafv2b  27937  dfafn5a  27938  el2wlkonotot1  28215  usg2spthonot0  28230  islshpsm  29617  islshpat  29654  lkrsc  29734  lfl1dim  29758  ldual1dim  29803  isat3  29944  glbconxN  30014  islln2  30147  islpln2  30172  islvol2  30216  cdlemg2cex  31227  diaglbN  31692  diblsmopel  31808  dihopelvalcpre  31885  xihopellsmN  31891  dihopellsm  31892  dihglbcpreN  31937  mapdval4N  32269  hdmapoc  32571
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 178  df-an 361
  Copyright terms: Public domain W3C validator