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

Theorem pm4.71rd 619
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 615 . 2  |-  ( ( ps  ->  ch )  <->  ( ps  <->  ( ch  /\  ps ) ) )
31, 2sylib 190 1  |-  ( ph  ->  ( ps  <->  ( ch  /\ 
ps ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 6    <-> wb 178    /\ wa 360
This theorem is referenced by:  2reu5  2948  ralss  3214  rexss  3215  reuhypd  4533  dfco2a  5160  feu  5355  funbrfv2b  5501  dffn5  5502  eqfnfv2  5557  dff4  5608  fmptco  5625  dff13  5717  exopxfr2  6118  brtpos  6177  dftpos3  6186  opiota  6256  erinxp  6701  qliftfun  6711  pw2f1olem  6934  infm3  9681  prime  10060  hashf1lem2  11360  smueqlem  12644  vdwmc2  12989  acsfiel  13519  subsubc  13690  ismgmid  14350  eqger  14630  eqgid  14632  gaorber  14725  psrbaglefi  16081  znleval  16471  bastop2  16695  elcls2  16774  maxlp  16841  restopn2  16871  restdis  16872  1stccn  17152  tx1cn  17266  tx2cn  17267  idqtop  17360  tgqtop  17366  filuni  17543  uffix2  17582  cnflf  17660  isfcls  17667  fclsopn  17672  cnfcf  17700  ptcmplem2  17710  xmeter  17942  imasf1oxms  17998  prdsbl  18000  caucfil  18672  shft2rab  18830  sca2rab  18834  mbfinf  18983  i1f1lem  19007  i1fres  19023  itg1climres  19032  mbfi1fseqlem4  19036  iblpos  19110  itgposval  19113  cnplimc  19200  ply1remlem  19511  plyremlem  19647  dvdsflsumcom  20391  fsumvma2  20416  vmasum  20418  logfac2  20419  chpchtsum  20421  logfaclbnd  20424  lgsquadlem1  20556  lgsquadlem2  20557  lgsquadlem3  20558  dchrisum0lem1  20628  pjpreeq  21938  elnlfn  22469  eupath2lem2  23275  eupath2  23277  predfz  23573  colinearalg  23914  dfoprab4pop  24404  fneval  25655  prter3  26118  rmydioph  26475  pw2f1ocnv  26498  bnj1171  28162  islshpat  28457  lfl1dim  28561  glbconxN  28817  cdlemefrs29bpre0  29835  dib1dim  30605  dib1dim2  30608  diclspsn  30634  dihopelvalcpre  30688  dih1dimatlem  30769  mapdordlem1a  31074  hdmapoc  31374
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10
This theorem depends on definitions:  df-bi 179  df-an 362
  Copyright terms: Public domain W3C validator