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

Theorem pm4.71ri 392
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 390 . 2  |-  ( (
ph  ->  ps )  <->  ( ph  <->  ( ps  /\  ph )
) )
31, 2mpbi 145 1  |-  ( ph  <->  ( ps  /\  ph )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 104    <-> wb 105
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  biadan2  456  anabs7  574  biadani  612  orabs  815  prlem2  975  sb6  1896  2moswapdc  2126  exsnrex  3646  eliunxp  4778  asymref  5026  elxp4  5128  elxp5  5129  dffun9  5257  funcnv  5289  funcnv3  5290  f1ompt  5680  eufnfv  5760  dff1o6  5790  abexex  6140  dfoprab4  6206  tpostpos  6278  erovlem  6640  elixp2  6715  xpsnen  6834  ctssdccl  7123  ltbtwnnq  7428  enq0enq  7443  prnmaxl  7500  prnminu  7501  elznn0nn  9280  zrevaddcl  9316  qrevaddcl  9657  climreu  11318  isprm3  12131  isprm4  12132  xpscf  12784  tgval2  13791  eltg2b  13794  isms2  14194
  Copyright terms: Public domain W3C validator