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:  ralss  3181  rexss  3182  reuhypd  4498  dfco2a  5125  feu  5320  funbrfv2b  5466  dffn5  5467  eqfnfv2  5522  dff4  5573  fmptco  5590  dff13  5682  exopxfr2  6083  brtpos  6142  dftpos3  6151  opiota  6221  erinxp  6666  qliftfun  6676  pw2f1olem  6899  infm3  9646  prime  10024  hashf1lem2  11324  smueqlem  12608  vdwmc2  12953  acsfiel  13483  subsubc  13654  ismgmid  14314  eqger  14594  eqgid  14596  gaorber  14689  psrbaglefi  16045  znleval  16435  bastop2  16659  elcls2  16738  maxlp  16805  restopn2  16835  restdis  16836  1stccn  17116  tx1cn  17230  tx2cn  17231  idqtop  17324  tgqtop  17330  filuni  17507  uffix2  17546  cnflf  17624  isfcls  17631  fclsopn  17636  cnfcf  17664  ptcmplem2  17674  xmeter  17906  imasf1oxms  17962  prdsbl  17964  caucfil  18636  shft2rab  18794  sca2rab  18798  mbfinf  18947  i1f1lem  18971  i1fres  18987  itg1climres  18996  mbfi1fseqlem4  19000  iblpos  19074  itgposval  19077  cnplimc  19164  ply1remlem  19475  plyremlem  19611  dvdsflsumcom  20355  fsumvma2  20380  vmasum  20382  logfac2  20383  chpchtsum  20385  logfaclbnd  20388  lgsquadlem1  20520  lgsquadlem2  20521  lgsquadlem3  20522  dchrisum0lem1  20592  pjpreeq  21902  elnlfn  22433  eupath2lem2  23239  eupath2  23241  predfz  23537  colinearalg  23878  dfoprab4pop  24368  fneval  25619  prter3  26082  rmydioph  26439  pw2f1ocnv  26462  bnj1171  28042  islshpat  28337  lfl1dim  28441  glbconxN  28697  cdlemefrs29bpre0  29715  dib1dim  30485  dib1dim2  30488  diclspsn  30514  dihopelvalcpre  30568  dih1dimatlem  30649  mapdordlem1a  30954  hdmapoc  31254
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