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

Theorem pm4.71i 377
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 375 . 2 ((𝜑𝜓) ↔ (𝜑 ↔ (𝜑𝜓)))
31, 2mpbi 137 1 (𝜑 ↔ (𝜑𝜓))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 101  wb 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105
This theorem depends on definitions:  df-bi 114
This theorem is referenced by:  pm4.24  381  anabs1  514  pm4.45  708  unidif0  3947  sucexb  4250  imadmrn  4705  dff1o2  5158  xpsnen  6325  dmaddpq  6534  dmmulpq  6535  eqreznegel  8645  xrnemnf  8799  xrnepnf  8800  elioopnf  8936  elioomnf  8937  elicopnf  8938  elxrge0  8947  bj-sucexg  10408
  Copyright terms: Public domain W3C validator