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

Theorem pm4.71i 371
 Description: Inference converting an implication to a biconditional with conjunction. Inference from Theorem *4.71 of [WhiteheadRussell] p. 120. (Contributed by NM, 4-Jan-2004.)
Hypothesis
Ref Expression
pm4.71i.1 (𝜑𝜓)
Assertion
Ref Expression
pm4.71i (𝜑 ↔ (𝜑𝜓))

Proof of Theorem pm4.71i
StepHypRef Expression
1 pm4.71i.1 . 2 (𝜑𝜓)
2 pm4.71 369 . 2 ((𝜑𝜓) ↔ (𝜑 ↔ (𝜑𝜓)))
31, 2mpbi 133 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:  pm4.24  375  anabs1  506  pm4.45  698  unidif0  3920  sucexb  4223  imadmrn  4678  dff1o2  5131  xpsnen  6295  dmaddpq  6477  dmmulpq  6478  eqreznegel  8549  xrnemnf  8699  xrnepnf  8700  elioopnf  8836  elioomnf  8837  elicopnf  8838  elxrge0  8847  bj-sucexg  10042
 Copyright terms: Public domain W3C validator