ILE Home 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  697  unidif0  3911  sucexb  4189  imadmrn  4621  dff1o2  5074  xpsnen  6231  dmaddpq  6363  dmmulpq  6364  eqreznegel  8325  xrnemnf  8469  xrnepnf  8470  elioopnf  8606  elioomnf  8607  elicopnf  8608  elxrge0  8617  bj-sucexg  9377
  Copyright terms: Public domain W3C validator