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 ) )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  pm4.24  399  anabs1  578  pm4.45  796  unidif0  4304  sucexb  4644  imadmrn  5136  dff1o2  5644  xpsnen  7119  dmaddpq  7747  dmmulpq  7748  eqreznegel  10024  xrnemnf  10190  xrnepnf  10191  elioopnf  10380  elioomnf  10381  elicopnf  10382  elxrge0  10391  dfrp2  10709  isprm2  12914  bj-sucexg  17114