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  3160  rexss  3161  reuhypd  4452  dfco2a  5079  feu  5274  funbrfv2b  5419  dffn5  5420  eqfnfv2  5475  dff4  5526  fmptco  5543  dff13  5635  exopxfr2  6036  brtpos  6095  dftpos3  6104  opiota  6174  erinxp  6619  qliftfun  6629  pw2f1olem  6851  infm3  9593  prime  9971  hashf1lem2  11271  smueqlem  12555  vdwmc2  12900  acsfiel  13401  subsubc  13571  ismgmid  14222  eqger  14502  eqgid  14504  gaorber  14597  psrbaglefi  15950  znleval  16340  bastop2  16564  elcls2  16643  maxlp  16710  restopn2  16740  restdis  16741  1stccn  17021  tx1cn  17135  tx2cn  17136  idqtop  17229  tgqtop  17235  filuni  17412  uffix2  17451  cnflf  17529  isfcls  17536  fclsopn  17541  cnfcf  17569  ptcmplem2  17579  xmeter  17811  imasf1oxms  17867  prdsbl  17869  caucfil  18541  shft2rab  18699  sca2rab  18703  mbfinf  18852  i1f1lem  18876  i1fres  18892  itg1climres  18901  mbfi1fseqlem4  18905  iblpos  18979  itgposval  18982  cnplimc  19069  ply1remlem  19380  plyremlem  19516  dvdsflsumcom  20260  fsumvma2  20285  vmasum  20287  logfac2  20288  chpchtsum  20290  logfaclbnd  20293  lgsquadlem1  20425  lgsquadlem2  20426  lgsquadlem3  20427  dchrisum0lem1  20497  pjpreeq  21807  elnlfn  22338  eupath2lem2  23073  eupath2  23075  predfz  23371  colinearalg  23712  dfoprab4pop  24202  fneval  25453  prter3  25916  rmydioph  26273  pw2f1ocnv  26296  bnj1171  27719  islshpat  27966  lfl1dim  28070  glbconxN  28326  cdlemefrs29bpre0  29344  dib1dim  30114  dib1dim2  30117  diclspsn  30143  dihopelvalcpre  30197  dih1dimatlem  30278  mapdordlem1a  30583  hdmapoc  30883
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