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

Theorem pm4.71ri 385
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 383 . 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-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  biadan2  445  anabs7  542  biadani  580  orabs  766  prlem2  923  sb6  1821  2moswapdc  2045  exsnrex  3505  eliunxp  4606  asymref  4850  elxp4  4952  elxp5  4953  dffun9  5078  funcnv  5109  funcnv3  5110  f1ompt  5489  eufnfv  5564  dff1o6  5593  abexex  5935  dfoprab4  6000  tpostpos  6067  erovlem  6424  elixp2  6499  xpsnen  6617  ltbtwnnq  7072  enq0enq  7087  prnmaxl  7144  prnminu  7145  elznn0nn  8862  zrevaddcl  8898  qrevaddcl  9228  climreu  10840  isprm3  11527  isprm4  11528  tgval2  11903  eltg2b  11906  isms2  12240
  Copyright terms: Public domain W3C validator