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

Theorem pm4.71rd 380
 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 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
pm4.71rd (𝜑 → (𝜓 ↔ (𝜒𝜓)))

Proof of Theorem pm4.71rd
StepHypRef Expression
1 pm4.71rd.1 . 2 (𝜑 → (𝜓𝜒))
2 pm4.71r 376 . 2 ((𝜓𝜒) ↔ (𝜓 ↔ (𝜒𝜓)))
31, 2sylib 131 1 (𝜑 → (𝜓 ↔ (𝜒𝜓)))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 101   ↔ wb 102 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105 This theorem depends on definitions:  df-bi 114 This theorem is referenced by:  ralss  3034  rexss  3035  reuhypd  4231  elxp4  4836  elxp5  4837  dfco2a  4849  feu  5100  funbrfv2b  5246  dffn5im  5247  eqfnfv2  5294  dff4im  5341  fmptco  5358  dff13  5435  f1od2  5884  mpt2xopovel  5887  brtposg  5900  dftpos3  5908  erinxp  6211  qliftfun  6219  genpdflem  6663  ltexprlemm  6756  prime  8396  oddnn02np1  10192  oddge22np1  10193  evennn02n  10194  evennn2n  10195
 Copyright terms: Public domain W3C validator