Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  pm4.71ri Unicode 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  452  anabs7  564  biadani  602  orabs  804  prlem2  959  sb6  1859  2moswapdc  2090  exsnrex  3574  eliunxp  4688  asymref  4934  elxp4  5036  elxp5  5037  dffun9  5162  funcnv  5194  funcnv3  5195  f1ompt  5581  eufnfv  5658  dff1o6  5687  abexex  6034  dfoprab4  6100  tpostpos  6171  erovlem  6531  elixp2  6606  xpsnen  6725  ctssdccl  7009  ltbtwnnq  7271  enq0enq  7286  prnmaxl  7343  prnminu  7344  elznn0nn  9115  zrevaddcl  9151  qrevaddcl  9486  climreu  11121  isprm3  11858  isprm4  11859  tgval2  12282  eltg2b  12285  isms2  12685
 Copyright terms: Public domain W3C validator