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

Step	Hyp	Ref	Expression
1		pm4.71ri.1	. 2 |- ( ph -> ps )
2		pm4.71r 382	. 2 |- ( ( ph -> ps ) <-> ( ph <-> ( ps /\ ph ) ) )
3	1, 2	mpbi 143	1 |- ( ph <-> ( ps /\ ph ) )

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  443  anabs7  538  orabs  760  prlem2  915  sb6  1807  2moswapdc  2031  exsnrex  3435  eliunxp  4493  asymref  4730  elxp4  4828  elxp5  4829  dffun9  4950  funcnv  4980  funcnv3  4981  f1ompt  5341  eufnfv  5410  dff1o6  5436  abexex  5773  dfoprab4  5838  tpostpos  5902  erovlem  6221  xpsnen  6318  ltbtwnnq  6606  enq0enq  6621  prnmaxl  6678  prnminu  6679  elznn0nn  8365  zrevaddcl  8401  qrevaddcl  8729  climreu  10136  isprm3  10500  isprm4  10501