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

Theorem pm4.71rd 617
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 613 . 2  |-  ( ( ps  ->  ch )  <->  ( ps  <->  ( ch  /\  ps ) ) )
31, 2sylib 189 1  |-  ( ph  ->  ( ps  <->  ( ch  /\ 
ps ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359
This theorem is referenced by:  2reu5  3134  ralss  3401  rexss  3402  reuhypd  4742  dfco2a  5362  feu  5611  funbrfv2b  5763  dffn5  5764  eqfnfv2  5820  dff4  5875  fmptco  5893  dff13  5996  exopxfr2  6403  mpt2xopovel  6463  brtpos  6480  dftpos3  6489  opiota  6527  erinxp  6970  qliftfun  6981  pw2f1olem  7204  infm3  9959  prime  10342  hashf1lem2  11697  smueqlem  12994  vdwmc2  13339  acsfiel  13871  subsubc  14042  ismgmid  14702  eqger  14982  eqgid  14984  gaorber  15077  psrbaglefi  16429  znleval  16827  bastop2  17051  elcls2  17130  maxlp  17203  restopn2  17233  restdis  17234  1stccn  17518  tx1cn  17633  tx2cn  17634  imasnopn  17714  imasncld  17715  imasncls  17716  idqtop  17730  tgqtop  17736  filuni  17909  uffix2  17948  cnflf  18026  isfcls  18033  fclsopn  18038  cnfcf  18066  ptcmplem2  18076  xmeter  18455  imasf1oxms  18511  prdsbl  18513  caucfil  19228  cfilucfil4OLD  19265  cfilucfil4  19266  shft2rab  19396  sca2rab  19400  mbfinf  19549  i1f1lem  19573  i1fres  19589  itg1climres  19598  mbfi1fseqlem4  19602  iblpos  19676  itgposval  19679  cnplimc  19766  ply1remlem  20077  plyremlem  20213  dvdsflsumcom  20965  fsumvma2  20990  vmasum  20992  logfac2  20993  chpchtsum  20995  logfaclbnd  20998  lgsquadlem1  21130  lgsquadlem2  21131  lgsquadlem3  21132  dchrisum0lem1  21202  nbgrael  21430  nbgraeledg  21434  nbgraf1olem1  21443  eupath2lem2  21692  eupath2  21694  pjpreeq  22892  elnlfn  23423  feqmptdf  24067  fmptcof2  24068  2ndpreima  24088  iocinioc2  24134  indpi1  24411  1stmbfm  24602  2ndmbfm  24603  predfz  25470  elfuns  25752  colinearalg  25841  areacirclem6  26277  fneval  26348  prter3  26712  rmydioph  27066  pw2f1ocnv  27089  funbrafv2b  27980  dfafn5a  27981  2spot2iun2spont  28301  frgraeu  28370  usgreg2spot  28383  bnj1171  29296  islshpat  29742  lfl1dim  29846  glbconxN  30102  cdlemefrs29bpre0  31120  dib1dim  31890  dib1dim2  31893  diclspsn  31919  dihopelvalcpre  31973  dih1dimatlem  32054  mapdordlem1a  32359  hdmapoc  32659
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 178  df-an 361
  Copyright terms: Public domain W3C validator