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

Theorem pm4.71ri 389
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 387 . 2  |-  ( (
ph  ->  ps )  <->  ( ph  <->  ( ps  /\  ph )
) )
31, 2mpbi 144 1  |-  ( ph  <->  ( ps  /\  ph )
)
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  451  anabs7  548  biadani  586  orabs  788  prlem2  943  sb6  1842  2moswapdc  2067  exsnrex  3536  eliunxp  4648  asymref  4894  elxp4  4996  elxp5  4997  dffun9  5122  funcnv  5154  funcnv3  5155  f1ompt  5539  eufnfv  5616  dff1o6  5645  abexex  5992  dfoprab4  6058  tpostpos  6129  erovlem  6489  elixp2  6564  xpsnen  6683  ctssdccl  6964  ltbtwnnq  7192  enq0enq  7207  prnmaxl  7264  prnminu  7265  elznn0nn  9036  zrevaddcl  9072  qrevaddcl  9404  climreu  11034  isprm3  11726  isprm4  11727  tgval2  12147  eltg2b  12150  isms2  12550
  Copyright terms: Public domain W3C validator