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  814  prlem2  974  sb6  1886  2moswapdc  2116  exsnrex  3633  eliunxp  4761  asymref  5009  elxp4  5111  elxp5  5112  dffun9  5240  funcnv  5272  funcnv3  5273  f1ompt  5662  eufnfv  5741  dff1o6  5770  abexex  6120  dfoprab4  6186  tpostpos  6258  erovlem  6620  elixp2  6695  xpsnen  6814  ctssdccl  7103  ltbtwnnq  7393  enq0enq  7408  prnmaxl  7465  prnminu  7466  elznn0nn  9243  zrevaddcl  9279  qrevaddcl  9620  climreu  11276  isprm3  12088  isprm4  12089  tgval2  13184  eltg2b  13187  isms2  13587
  Copyright terms: Public domain W3C validator