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  2975  ralss  3241  rexss  3242  reuhypd  4563  dfco2a  5175  feu  5419  funbrfv2b  5569  dffn5  5570  eqfnfv2  5625  dff4  5676  fmptco  5693  dff13  5785  exopxfr2  6186  brtpos  6245  dftpos3  6254  opiota  6292  erinxp  6735  qliftfun  6745  pw2f1olem  6968  infm3  9715  prime  10094  hashf1lem2  11396  smueqlem  12683  vdwmc2  13028  acsfiel  13558  subsubc  13729  ismgmid  14389  eqger  14669  eqgid  14671  gaorber  14764  psrbaglefi  16120  znleval  16510  bastop2  16734  elcls2  16813  maxlp  16880  restopn2  16910  restdis  16911  1stccn  17191  tx1cn  17305  tx2cn  17306  idqtop  17399  tgqtop  17405  filuni  17582  uffix2  17621  cnflf  17699  isfcls  17706  fclsopn  17711  cnfcf  17739  ptcmplem2  17749  xmeter  17981  imasf1oxms  18037  prdsbl  18039  caucfil  18711  shft2rab  18869  sca2rab  18873  mbfinf  19022  i1f1lem  19046  i1fres  19062  itg1climres  19071  mbfi1fseqlem4  19075  iblpos  19149  itgposval  19152  cnplimc  19239  ply1remlem  19550  plyremlem  19686  dvdsflsumcom  20430  fsumvma2  20455  vmasum  20457  logfac2  20458  chpchtsum  20460  logfaclbnd  20463  lgsquadlem1  20595  lgsquadlem2  20596  lgsquadlem3  20597  dchrisum0lem1  20667  pjpreeq  21979  elnlfn  22510  xppreima  23213  feqmptdf  23230  fmptcof2  23231  iocinioc2  23274  1stmbfm  23567  2ndmbfm  23568  indpi1  23607  eupath2lem2  23904  eupath2  23906  predfz  24205  colinearalg  24540  areacirclem6  24941  dfoprab4pop  25048  fneval  26298  prter3  26761  rmydioph  27118  pw2f1ocnv  27141  funbrafv2b  28032  dfafn5a  28033  mpt2xopovel  28097  nbgrael  28152  nbgraeledg  28156  bnj1171  29103  islshpat  29280  lfl1dim  29384  glbconxN  29640  cdlemefrs29bpre0  30658  dib1dim  31428  dib1dim2  31431  diclspsn  31457  dihopelvalcpre  31511  dih1dimatlem  31592  mapdordlem1a  31897  hdmapoc  32197
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