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  2681  reubida  2850  rmobida  2855  mpteq12f  4245  reuhypd  4709  funbrfv2b  5730  dffn5  5731  eqfnfv2  5787  fmptco  5860  dff13  5963  mpt2eq123dva  6094  mpt2eq3dva  6097  fnwelem  6420  mpt2xopovel  6430  opiota  6494  riotabidva  6525  oeeui  6804  omabs  6849  qliftfun  6948  erovlem  6959  xpcomco  7157  pw2f1olem  7171  elfi2  7377  cardval2  7834  dfac2  7967  cflim3  8098  iundom2g  8371  fpwwe2lem8  8468  fpwwe2lem12  8472  ltexpi  8735  ordpipq  8775  axrrecex  8994  nnunb  10173  zrevaddcl  10277  qrevaddcl  10552  icoshft  10975  fznn  11070  fznnfl  11198  fz1isolem  11665  2shfti  11850  limsupgle  12226  ello12  12265  elo12  12276  isercoll  12416  sumeq2ii  12442  fsum2dlem  12509  bitsmod  12903  bitscmp  12905  pwsle  13669  imasleval  13721  acsfiel  13834  ismon2  13915  isepi2  13922  oppcsect  13954  subsubc  14005  funcpropd  14052  fullpropd  14072  fucsect  14124  setcsect  14199  pltval3  14379  ismgmid  14665  grpidpropd  14677  mhmpropd  14699  issubm2  14704  subgacs  14930  eqgid  14947  pgpfi2  15195  eqgabl  15409  iscyggen2  15446  cyggenod  15449  eldprd  15517  subgdmdprd  15547  dprd2d2  15557  rngpropd  15650  crngunit  15722  dvdsrpropd  15756  drngpropd  15817  issubrg3  15851  lsslss  15992  lsspropd  16048  lmhmpropd  16100  lbspropd  16126  aspval2  16360  znleval  16790  znunithash  16800  pjdm2  16893  bastop2  17014  elcls2  17093  neiptopreu  17152  maxlp  17165  restopn2  17195  iscnp3  17262  subbascn  17272  lmbr2  17277  kgencn  17541  kgencn2  17542  hauseqlcld  17631  txlm  17633  txkgen  17637  xkoptsub  17639  idqtop  17691  tgqtop  17697  qtopcld  17698  elmptrab  17812  flimopn  17960  fbflim  17961  fbflim2  17962  flimrest  17968  flffbas  17980  flftg  17981  cnflf  17987  cnflf2  17988  txflf  17991  isfcls  17994  fclsopn  17999  fclsbas  18006  fclsrest  18009  fcfnei  18020  cnfcf  18027  ptcmplem2  18037  tgphaus  18099  tsmssubm  18125  isucn2  18262  ismet2  18316  xblpnfps  18378  xblpnf  18379  blin  18404  blres  18414  elmopn2  18428  imasf1obl  18471  imasf1oxms  18472  prdsbl  18474  neibl  18484  metrest  18507  metcnp3  18523  metcnp  18524  metcnp2  18525  metcn  18526  txmetcnp  18530  txmetcn  18531  metuel2  18562  metucnOLD  18571  metucn  18572  ngppropd  18631  cnbl0  18761  cnblcld  18762  bl2ioo  18776  xrtgioo  18790  elcncf2  18873  cncfmet  18891  nmhmcn  19081  lmmbr  19164  lmmbr2  19165  iscfil2  19172  iscau2  19183  iscau3  19184  lmclim  19208  shft2rab  19357  sca2rab  19361  mbfeqalem  19487  mbfmulc2lem  19492  mbfmax  19494  mbfposr  19497  mbfimaopnlem  19500  mbfaddlem  19505  mbfsup  19509  mbfinf  19510  i1fmullem  19539  i1fmulclem  19547  i1fres  19550  itg1climres  19559  mbfi1fseqlem4  19563  ibllem  19609  ellimc2  19717  ellimc3  19719  limcflf  19721  cnplimc  19727  cnlimc  19728  dvreslem  19749  ply1remlem  20038  fta1glem2  20042  ofmulrt  20152  plyremlem  20174  ulm2  20254  mcubic  20640  cubic2  20641  dvdsflsumcom  20926  fsumvma  20950  fsumvma2  20951  vmasum  20953  logfaclbnd  20959  dchrelbas2  20974  dchrelbas3  20975  dchrelbas4  20980  lgsquadlem1  21091  lgsquadlem2  21092  nbgrael  21391  nbcusgra  21425  eupath2  21655  isblo2  22237  ubthlem1  22325  h2hlm  22436  pjpreeq  22853  elnlfn  23384  reuxfr4d  23930  feqmptdf  24028  fmptcof2  24029  funcnvmpt  24036  gsumpropd2lem  24173  itgeq12dv  24594  orvcgteel  24678  prodeq2ii  25192  dfrdg2  25366  preduz  25414  predfz  25417  broutsideof3  25964  cnambfre  26154  itg2gt0cn  26159  areacirclem6  26186  isfne4b  26240  filnetlem4  26300  isdrngo3  26465  isidlc  26515  prter3  26621  ellz1  26715  rmydioph  26975  rmxdioph  26977  expdiophlem1  26982  expdioph  26984  pw2f1ocnv  26998  dnwech  27013  islinds2  27151  sdrgacs  27377  pm14.123b  27494  rfcnpre1  27557  rfcnpre2  27569  rfcnpre3  27571  rfcnpre4  27572  climreeq  27606  funbrafv2b  27890  dfafn5a  27891  el2wlkonotot1  28071  usg2spthonot0  28086  islshpsm  29463  islshpat  29500  lkrsc  29580  lfl1dim  29604  ldual1dim  29649  isat3  29790  glbconxN  29860  islln2  29993  islpln2  30018  islvol2  30062  cdlemg2cex  31073  diaglbN  31538  diblsmopel  31654  dihopelvalcpre  31731  xihopellsmN  31737  dihopellsm  31738  dihglbcpreN  31783  mapdval4N  32115  hdmapoc  32417
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