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  3085  rexss  3086  reuhypd  4284  elxp4  4905  elxp5  4906  dfco2a  4918  feu  5177  funbrfv2b  5333  dffn5im  5334  eqfnfv2  5382  dff4im  5429  fmptco  5448  dff13  5529  f1od2  5982  mpt2xopovel  5988  brtposg  6001  dftpos3  6009  erinxp  6346  qliftfun  6354  genpdflem  7045  ltexprlemm  7138  prime  8815  oddnn02np1  10962  oddge22np1  10963  evennn02n  10964  evennn2n  10965
  Copyright terms: Public domain W3C validator