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  4306  sucexb  4646  imadmrn  5139  dff1o2  5647  xpsnen  7125  dmaddpq  7752  dmmulpq  7753  eqreznegel  10029  xrnemnf  10195  xrnepnf  10196  elioopnf  10385  elioomnf  10386  elicopnf  10387  elxrge0  10396  dfrp2  10714  isprm2  12919  bj-sucexg  17170