Theorem pm4.71i 395

Description: Inference converting an implication to a biconditional with conjunction. Inference from Theorem *4.71 of [WhiteheadRussell] p. 120. (Contributed by NM, 4-Jan-2004.)

Hypothesis

Ref	Expression
pm4.71i.1	|- ( ph -> ps )

Assertion

Ref	Expression
pm4.71i	|- ( ph <-> ( ph /\ ps ) )

Proof of Theorem pm4.71i

Step	Hyp	Ref	Expression
1		pm4.71i.1	. 2 |- ( ph -> ps )
2		pm4.71 393	. 2 |- ( ( ph -> ps ) <-> ( ph <-> ( ph /\ ps ) ) )
3	1, 2	mpbi 145	1 |- ( ph <-> ( ph /\ ps ) )

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:  pm4.24  399  anabs1  578  pm4.45  796  unidif0  4302  sucexb  4642  imadmrn  5134  dff1o2  5642  xpsnen  7112  dmaddpq  7739  dmmulpq  7740  eqreznegel  9996  xrnemnf  10161  xrnepnf  10162  elioopnf  10351  elioomnf  10352  elicopnf  10353  elxrge0  10362  dfrp2  10679  isprm2  12876  bj-sucexg  16865