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

Theorem pm4.71ri 387
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 385 . 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-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  biadan2  449  anabs7  546  biadani  584  orabs  786  prlem2  941  sb6  1840  2moswapdc  2065  exsnrex  3532  eliunxp  4638  asymref  4882  elxp4  4984  elxp5  4985  dffun9  5110  funcnv  5142  funcnv3  5143  f1ompt  5525  eufnfv  5602  dff1o6  5631  abexex  5978  dfoprab4  6044  tpostpos  6115  erovlem  6475  elixp2  6550  xpsnen  6668  ctssdccl  6948  ltbtwnnq  7172  enq0enq  7187  prnmaxl  7244  prnminu  7245  elznn0nn  8972  zrevaddcl  9008  qrevaddcl  9338  climreu  10958  isprm3  11645  isprm4  11646  tgval2  12063  eltg2b  12066  isms2  12443
  Copyright terms: Public domain W3C validator