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

Theorem pm4.71ri 390
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 388 . 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  453  anabs7  569  biadani  607  orabs  809  prlem2  969  sb6  1879  2moswapdc  2109  exsnrex  3623  eliunxp  4748  asymref  4994  elxp4  5096  elxp5  5097  dffun9  5225  funcnv  5257  funcnv3  5258  f1ompt  5645  eufnfv  5724  dff1o6  5753  abexex  6103  dfoprab4  6169  tpostpos  6241  erovlem  6603  elixp2  6678  xpsnen  6797  ctssdccl  7086  ltbtwnnq  7371  enq0enq  7386  prnmaxl  7443  prnminu  7444  elznn0nn  9219  zrevaddcl  9255  qrevaddcl  9596  climreu  11253  isprm3  12065  isprm4  12066  tgval2  12810  eltg2b  12813  isms2  13213
  Copyright terms: Public domain W3C validator