ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  pm4.71ri Structured version   Unicode 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  726  prlem2  880  sb6  1763  2moswapdc  1987  exsnrex  3404  eliunxp  4418  asymref  4653  elxp4  4751  elxp5  4752  dffun9  4873  funcnv  4903  funcnv3  4904  f1ompt  5263  eufnfv  5332  dff1o6  5359  abexex  5695  dfoprab4  5760  tpostpos  5820  erovlem  6134  xpsnen  6231  ltbtwnnq  6399  enq0enq  6413  prnmaxl  6470  prnminu  6471  elznn0nn  7995  zrevaddcl  8031  qrevaddcl  8313
  Copyright terms: Public domain W3C validator