Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  pm4.71ri 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  429  anabs7  508  orabs  727  prlem2  881  sb6  1766  2moswapdc  1990  exsnrex  3413  eliunxp  4475  asymref  4710  elxp4  4808  elxp5  4809  dffun9  4930  funcnv  4960  funcnv3  4961  f1ompt  5320  eufnfv  5389  dff1o6  5416  abexex  5753  dfoprab4  5818  tpostpos  5879  erovlem  6198  xpsnen  6295  ltbtwnnq  6514  enq0enq  6529  prnmaxl  6586  prnminu  6587  elznn0nn  8259  zrevaddcl  8295  qrevaddcl  8578  climreu  9818
 Copyright terms: Public domain W3C validator