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

Proof of Theorem pm4.71rd
StepHypRef Expression
1 pm4.71rd.1 . 2 (𝜑 → (𝜓𝜒))
2 pm4.71r 387 . 2 ((𝜓𝜒) ↔ (𝜓 ↔ (𝜒𝜓)))
31, 2sylib 121 1 (𝜑 → (𝜓 ↔ (𝜒𝜓)))
 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  3163  rexss  3164  reuhypd  4392  elxp4  5026  elxp5  5027  dfco2a  5039  feu  5305  funbrfv2b  5466  dffn5im  5467  eqfnfv2  5519  dff4im  5566  fmptco  5586  dff13  5669  f1od2  6132  mpoxopovel  6138  brtposg  6151  dftpos3  6159  erinxp  6503  qliftfun  6511  genpdflem  7322  ltexprlemm  7415  prime  9157  oddnn02np1  11584  oddge22np1  11585  evennn02n  11586  evennn2n  11587  bastop2  12263  restopn2  12362  restdis  12363  tx1cn  12448  tx2cn  12449  imasnopn  12478  xmeter  12615
 Copyright terms: Public domain W3C validator