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

Theorem pm4.71i 383
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 381 . 2 ((𝜑𝜓) ↔ (𝜑 ↔ (𝜑𝜓)))
31, 2mpbi 143 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:  pm4.24  387  anabs1  539  pm4.45  733  unidif0  4000  sucexb  4312  imadmrn  4779  dff1o2  5252  xpsnen  6527  dmaddpq  6928  dmmulpq  6929  eqreznegel  9089  xrnemnf  9238  xrnepnf  9239  elioopnf  9375  elioomnf  9376  elicopnf  9377  elxrge0  9386  isprm2  11364  bj-sucexg  11696
  Copyright terms: Public domain W3C validator