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

Theorem pm4.71ri 384
 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 382 . 2 ((𝜑𝜓) ↔ (𝜑 ↔ (𝜓𝜑)))
31, 2mpbi 143 1 (𝜑 ↔ (𝜓𝜑))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 102   ↔ wb 103 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106 This theorem depends on definitions:  df-bi 115 This theorem is referenced by:  biadan2  444  anabs7  539  orabs  761  prlem2  916  sb6  1809  2moswapdc  2033  exsnrex  3453  eliunxp  4523  asymref  4760  elxp4  4858  elxp5  4859  dffun9  4980  funcnv  5011  funcnv3  5012  f1ompt  5373  eufnfv  5442  dff1o6  5468  abexex  5805  dfoprab4  5870  tpostpos  5934  erovlem  6286  xpsnen  6387  ltbtwnnq  6738  enq0enq  6753  prnmaxl  6810  prnminu  6811  elznn0nn  8516  zrevaddcl  8552  qrevaddcl  8880  climreu  10355  isprm3  10725  isprm4  10726
 Copyright terms: Public domain W3C validator