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

Theorem pm4.71ri 372
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 370 . 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:  biadan2  432  anabs7  495  orabs  714  prlem2  869  sb6  1748  2moswapdc  1972  exsnrex  3387  eliunxp  4402  asymref  4637  elxp4  4735  elxp5  4736  dffun9  4856  funcnv  4886  funcnv3  4887  f1ompt  5245  eufnfv  5314  dff1o6  5341  abexex  5676  dfoprab4  5741  tpostpos  5801  erovlem  6109  ltbtwnnq  6273  enq0enq  6286  prnmaxl  6342  prnminu  6343
  Copyright terms: Public domain W3C validator