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  3133  rexss  3134  reuhypd  4362  elxp4  4996  elxp5  4997  dfco2a  5009  feu  5275  funbrfv2b  5434  dffn5im  5435  eqfnfv2  5487  dff4im  5534  fmptco  5554  dff13  5637  f1od2  6100  mpoxopovel  6106  brtposg  6119  dftpos3  6127  erinxp  6471  qliftfun  6479  genpdflem  7283  ltexprlemm  7376  prime  9118  oddnn02np1  11504  oddge22np1  11505  evennn02n  11506  evennn2n  11507  bastop2  12180  restopn2  12279  restdis  12280  tx1cn  12365  tx2cn  12366  imasnopn  12395  xmeter  12532
  Copyright terms: Public domain W3C validator