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  2974  ralss  3240  rexss  3241  reuhypd  4560  dfco2a  5171  feu  5383  funbrfv2b  5529  dffn5  5530  eqfnfv2  5585  dff4  5636  fmptco  5653  dff13  5745  exopxfr2  6146  brtpos  6205  dftpos3  6214  opiota  6284  erinxp  6729  qliftfun  6739  pw2f1olem  6962  infm3  9709  prime  10088  hashf1lem2  11390  smueqlem  12677  vdwmc2  13022  acsfiel  13552  subsubc  13723  ismgmid  14383  eqger  14663  eqgid  14665  gaorber  14758  psrbaglefi  16114  znleval  16504  bastop2  16728  elcls2  16807  maxlp  16874  restopn2  16904  restdis  16905  1stccn  17185  tx1cn  17299  tx2cn  17300  idqtop  17393  tgqtop  17399  filuni  17576  uffix2  17615  cnflf  17693  isfcls  17700  fclsopn  17705  cnfcf  17733  ptcmplem2  17743  xmeter  17975  imasf1oxms  18031  prdsbl  18033  caucfil  18705  shft2rab  18863  sca2rab  18867  mbfinf  19016  i1f1lem  19040  i1fres  19056  itg1climres  19065  mbfi1fseqlem4  19069  iblpos  19143  itgposval  19146  cnplimc  19233  ply1remlem  19544  plyremlem  19680  dvdsflsumcom  20424  fsumvma2  20449  vmasum  20451  logfac2  20452  chpchtsum  20454  logfaclbnd  20457  lgsquadlem1  20589  lgsquadlem2  20590  lgsquadlem3  20591  dchrisum0lem1  20661  pjpreeq  21973  elnlfn  22504  eupath2lem2  23309  eupath2  23311  predfz  23607  colinearalg  23948  areacirclem6  24340  dfoprab4pop  24447  fneval  25698  prter3  26161  rmydioph  26518  pw2f1ocnv  26541  funbrafv2b  27412  dfafn5a  27413  bnj1171  28309  islshpat  28486  lfl1dim  28590  glbconxN  28846  cdlemefrs29bpre0  29864  dib1dim  30634  dib1dim2  30637  diclspsn  30663  dihopelvalcpre  30717  dih1dimatlem  30798  mapdordlem1a  31103  hdmapoc  31403
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