MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pm4.71rd 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  3085  ralss  3352  rexss  3353  reuhypd  4690  dfco2a  5310  feu  5559  funbrfv2b  5710  dffn5  5711  eqfnfv2  5767  dff4  5822  fmptco  5840  dff13  5943  exopxfr2  6350  mpt2xopovel  6407  brtpos  6424  dftpos3  6433  opiota  6471  erinxp  6914  qliftfun  6925  pw2f1olem  7148  infm3  9899  prime  10282  hashf1lem2  11632  smueqlem  12929  vdwmc2  13274  acsfiel  13806  subsubc  13977  ismgmid  14637  eqger  14917  eqgid  14919  gaorber  15012  psrbaglefi  16364  znleval  16758  bastop2  16982  elcls2  17061  maxlp  17133  restopn2  17163  restdis  17164  1stccn  17447  tx1cn  17562  tx2cn  17563  imasnopn  17643  imasncld  17644  imasncls  17645  idqtop  17659  tgqtop  17665  filuni  17838  uffix2  17877  cnflf  17955  isfcls  17962  fclsopn  17967  cnfcf  17995  ptcmplem2  18005  xmeter  18353  imasf1oxms  18409  prdsbl  18411  caucfil  19107  cfilucfil4  19143  shft2rab  19271  sca2rab  19275  mbfinf  19424  i1f1lem  19448  i1fres  19464  itg1climres  19473  mbfi1fseqlem4  19477  iblpos  19551  itgposval  19554  cnplimc  19641  ply1remlem  19952  plyremlem  20088  dvdsflsumcom  20840  fsumvma2  20865  vmasum  20867  logfac2  20868  chpchtsum  20870  logfaclbnd  20873  lgsquadlem1  21005  lgsquadlem2  21006  lgsquadlem3  21007  dchrisum0lem1  21077  nbgrael  21304  nbgraeledg  21308  nbgraf1olem1  21317  eupath2lem2  21548  eupath2  21550  pjpreeq  22748  elnlfn  23279  feqmptdf  23917  fmptcof2  23918  2ndpreima  23937  iocinioc2  23978  indpi1  24215  1stmbfm  24404  2ndmbfm  24405  predfz  25227  colinearalg  25563  areacirclem6  25987  fneval  26058  prter3  26422  rmydioph  26776  pw2f1ocnv  26799  funbrafv2b  27692  dfafn5a  27693  bnj1171  28707  islshpat  29132  lfl1dim  29236  glbconxN  29492  cdlemefrs29bpre0  30510  dib1dim  31280  dib1dim2  31283  diclspsn  31309  dihopelvalcpre  31363  dih1dimatlem  31444  mapdordlem1a  31749  hdmapoc  32049
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