ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  pm4.71rd Unicode version

Theorem pm4.71rd 386
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 382 . 2  |-  ( ( ps  ->  ch )  <->  ( ps  <->  ( ch  /\  ps ) ) )
31, 2sylib 120 1  |-  ( ph  ->  ( ps  <->  ( ch  /\ 
ps ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 102    <-> wb 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  ralss  3061  rexss  3062  reuhypd  4229  elxp4  4838  elxp5  4839  dfco2a  4851  feu  5103  funbrfv2b  5250  dffn5im  5251  eqfnfv2  5298  dff4im  5345  fmptco  5362  dff13  5439  f1od2  5887  mpt2xopovel  5890  brtposg  5903  dftpos3  5911  erinxp  6246  qliftfun  6254  genpdflem  6759  ltexprlemm  6852  prime  8527  oddnn02np1  10424  oddge22np1  10425  evennn02n  10426  evennn2n  10427
  Copyright terms: Public domain W3C validator