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

Theorem pm4.71rd 374
 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 370 . 2 ((𝜓𝜒) ↔ (𝜓 ↔ (𝜒𝜓)))
31, 2sylib 127 1 (𝜑 → (𝜓 ↔ (𝜒𝜓)))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 97   ↔ wb 98 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101 This theorem depends on definitions:  df-bi 110 This theorem is referenced by:  ralss  3006  rexss  3007  reuhypd  4203  elxp4  4808  elxp5  4809  dfco2a  4821  feu  5072  funbrfv2b  5218  dffn5im  5219  eqfnfv2  5266  dff4im  5313  fmptco  5330  dff13  5407  mpt2xopovel  5856  brtposg  5869  dftpos3  5877  erinxp  6180  qliftfun  6188  genpdflem  6605  ltexprlemm  6698  prime  8337
 Copyright terms: Public domain W3C validator