MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pm4.71rd Unicode version

Theorem pm4.71rd 616
Description: Deduction converting an implication to a biconditional with conjunction. Deduction from Theorem *4.71 of [WhiteheadRussell] p. 120. (Contributed by NM, 10-Feb-2005.)
Hypothesis
Ref Expression
pm4.71rd.1  |-  ( ph  ->  ( ps  ->  ch ) )
Assertion
Ref Expression
pm4.71rd  |-  ( ph  ->  ( ps  <->  ( ch  /\ 
ps ) ) )

Proof of Theorem pm4.71rd
StepHypRef Expression
1 pm4.71rd.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
2 pm4.71r 612 . 2  |-  ( ( ps  ->  ch )  <->  ( ps  <->  ( ch  /\  ps ) ) )
31, 2sylib 188 1  |-  ( ph  ->  ( ps  <->  ( ch  /\ 
ps ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358
This theorem is referenced by:  2reu5  2986  ralss  3252  rexss  3253  reuhypd  4577  dfco2a  5189  feu  5433  funbrfv2b  5583  dffn5  5584  eqfnfv2  5639  dff4  5690  fmptco  5707  dff13  5799  exopxfr2  6200  brtpos  6259  dftpos3  6268  opiota  6306  erinxp  6749  qliftfun  6759  pw2f1olem  6982  infm3  9729  prime  10108  hashf1lem2  11410  smueqlem  12697  vdwmc2  13042  acsfiel  13572  subsubc  13743  ismgmid  14403  eqger  14683  eqgid  14685  gaorber  14778  psrbaglefi  16134  znleval  16524  bastop2  16748  elcls2  16827  maxlp  16894  restopn2  16924  restdis  16925  1stccn  17205  tx1cn  17319  tx2cn  17320  idqtop  17413  tgqtop  17419  filuni  17596  uffix2  17635  cnflf  17713  isfcls  17720  fclsopn  17725  cnfcf  17753  ptcmplem2  17763  xmeter  17995  imasf1oxms  18051  prdsbl  18053  caucfil  18725  shft2rab  18883  sca2rab  18887  mbfinf  19036  i1f1lem  19060  i1fres  19076  itg1climres  19085  mbfi1fseqlem4  19089  iblpos  19163  itgposval  19166  cnplimc  19253  ply1remlem  19564  plyremlem  19700  dvdsflsumcom  20444  fsumvma2  20469  vmasum  20471  logfac2  20472  chpchtsum  20474  logfaclbnd  20477  lgsquadlem1  20609  lgsquadlem2  20610  lgsquadlem3  20611  dchrisum0lem1  20681  pjpreeq  21993  elnlfn  22524  xppreima  23226  feqmptdf  23243  fmptcof2  23244  iocinioc2  23287  1stmbfm  23580  2ndmbfm  23581  indpi1  23620  eupath2lem2  23917  eupath2  23919  predfz  24274  colinearalg  24610  areacirclem6  25033  dfoprab4pop  25140  fneval  26390  prter3  26853  rmydioph  27210  pw2f1ocnv  27233  funbrafv2b  28127  dfafn5a  28128  mpt2xopovel  28202  nbgrael  28275  nbgraeledg  28279  bnj1171  29346  islshpat  29829  lfl1dim  29933  glbconxN  30189  cdlemefrs29bpre0  31207  dib1dim  31977  dib1dim2  31980  diclspsn  32006  dihopelvalcpre  32060  dih1dimatlem  32141  mapdordlem1a  32446  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