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

Theorem pm4.71ri 384
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 382 . 2  |-  ( (
ph  ->  ps )  <->  ( ph  <->  ( ps  /\  ph )
) )
31, 2mpbi 143 1  |-  ( ph  <->  ( ps  /\  ph )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 102    <-> wb 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  biadan2  444  anabs7  541  orabs  763  prlem2  920  sb6  1814  2moswapdc  2038  exsnrex  3480  eliunxp  4563  asymref  4804  elxp4  4905  elxp5  4906  dffun9  5030  funcnv  5061  funcnv3  5062  f1ompt  5434  eufnfv  5507  dff1o6  5537  abexex  5879  dfoprab4  5944  tpostpos  6011  erovlem  6364  xpsnen  6517  ltbtwnnq  6954  enq0enq  6969  prnmaxl  7026  prnminu  7027  elznn0nn  8734  zrevaddcl  8770  qrevaddcl  9098  climreu  10649  isprm3  11182  isprm4  11183
  Copyright terms: Public domain W3C validator