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

Theorem pm4.71rd 391
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 387 . 2  |-  ( ( ps  ->  ch )  <->  ( ps  <->  ( ch  /\  ps ) ) )
31, 2sylib 121 1  |-  ( ph  ->  ( ps  <->  ( ch  /\ 
ps ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    <-> wb 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  ralss  3158  rexss  3159  reuhypd  4387  elxp4  5021  elxp5  5022  dfco2a  5034  feu  5300  funbrfv2b  5459  dffn5im  5460  eqfnfv2  5512  dff4im  5559  fmptco  5579  dff13  5662  f1od2  6125  mpoxopovel  6131  brtposg  6144  dftpos3  6152  erinxp  6496  qliftfun  6504  genpdflem  7308  ltexprlemm  7401  prime  9143  oddnn02np1  11562  oddge22np1  11563  evennn02n  11564  evennn2n  11565  bastop2  12238  restopn2  12337  restdis  12338  tx1cn  12423  tx2cn  12424  imasnopn  12453  xmeter  12590
  Copyright terms: Public domain W3C validator