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

Theorem pm4.71ri 378
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  |-  ( ph  ->  ps )
Assertion
Ref Expression
pm4.71ri  |-  ( ph  <->  ( ps  /\  ph )
)

Proof of Theorem pm4.71ri
StepHypRef Expression
1 pm4.71ri.1 . 2  |-  ( ph  ->  ps )
2 pm4.71r 376 . 2  |-  ( (
ph  ->  ps )  <->  ( ph  <->  ( ps  /\  ph )
) )
31, 2mpbi 137 1  |-  ( ph  <->  ( ps  /\  ph )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 101    <-> wb 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105
This theorem depends on definitions:  df-bi 114
This theorem is referenced by:  biadan2  437  anabs7  516  orabs  738  prlem2  892  sb6  1782  2moswapdc  2006  exsnrex  3441  eliunxp  4503  asymref  4738  elxp4  4836  elxp5  4837  dffun9  4958  funcnv  4988  funcnv3  4989  f1ompt  5348  eufnfv  5417  dff1o6  5444  abexex  5781  dfoprab4  5846  tpostpos  5910  erovlem  6229  xpsnen  6326  ltbtwnnq  6572  enq0enq  6587  prnmaxl  6644  prnminu  6645  elznn0nn  8316  zrevaddcl  8352  qrevaddcl  8676  climreu  10049
  Copyright terms: Public domain W3C validator