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

Theorem pm4.71ri 389
 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 387 . 2 ((𝜑𝜓) ↔ (𝜑 ↔ (𝜓𝜑)))
31, 2mpbi 144 1 (𝜑 ↔ (𝜓𝜑))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107 This theorem depends on definitions:  df-bi 116 This theorem is referenced by:  biadan2  451  anabs7  563  biadani  601  orabs  803  prlem2  958  sb6  1858  2moswapdc  2089  exsnrex  3566  eliunxp  4678  asymref  4924  elxp4  5026  elxp5  5027  dffun9  5152  funcnv  5184  funcnv3  5185  f1ompt  5571  eufnfv  5648  dff1o6  5677  abexex  6024  dfoprab4  6090  tpostpos  6161  erovlem  6521  elixp2  6596  xpsnen  6715  ctssdccl  6996  ltbtwnnq  7231  enq0enq  7246  prnmaxl  7303  prnminu  7304  elznn0nn  9075  zrevaddcl  9111  qrevaddcl  9443  climreu  11073  isprm3  11806  isprm4  11807  tgval2  12230  eltg2b  12233  isms2  12633
 Copyright terms: Public domain W3C validator