ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  pm4.71rd GIF 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 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
pm4.71rd (𝜑 → (𝜓 ↔ (𝜒𝜓)))

Proof of Theorem pm4.71rd
StepHypRef Expression
1 pm4.71rd.1 . 2 (𝜑 → (𝜓𝜒))
2 pm4.71r 382 . 2 ((𝜓𝜒) ↔ (𝜓 ↔ (𝜒𝜓)))
31, 2sylib 120 1 (𝜑 → (𝜓 ↔ (𝜒𝜓)))
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  3087  rexss  3088  reuhypd  4293  elxp4  4918  elxp5  4919  dfco2a  4931  feu  5193  funbrfv2b  5349  dffn5im  5350  eqfnfv2  5398  dff4im  5445  fmptco  5464  dff13  5547  f1od2  6000  mpt2xopovel  6006  brtposg  6019  dftpos3  6027  erinxp  6366  qliftfun  6374  genpdflem  7066  ltexprlemm  7159  prime  8845  oddnn02np1  11158  oddge22np1  11159  evennn02n  11160  evennn2n  11161
  Copyright terms: Public domain W3C validator