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

Theorem pm4.71ri 378
Description: Inference converting an implication to a biconditional with conjunction. Inference from Theorem *4.71 of [WhiteheadRussell] p. 120 (with conjunct reversed). (Contributed by NM, 1-Dec-2003.)
Hypothesis
Ref Expression
pm4.71ri.1 (𝜑𝜓)
Assertion
Ref Expression
pm4.71ri (𝜑 ↔ (𝜓𝜑))

Proof of Theorem pm4.71ri
StepHypRef Expression
1 pm4.71ri.1 . 2 (𝜑𝜓)
2 pm4.71r 376 . 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:  biadan2  437  anabs7  516  orabs  738  prlem2  892  sb6  1782  2moswapdc  2006  exsnrex  3440  eliunxp  4502  asymref  4737  elxp4  4835  elxp5  4836  dffun9  4957  funcnv  4987  funcnv3  4988  f1ompt  5347  eufnfv  5416  dff1o6  5443  abexex  5780  dfoprab4  5845  tpostpos  5909  erovlem  6228  xpsnen  6325  ltbtwnnq  6571  enq0enq  6586  prnmaxl  6643  prnminu  6644  elznn0nn  8315  zrevaddcl  8351  qrevaddcl  8675  climreu  10041
  Copyright terms: Public domain W3C validator