Theorem pm4.71i 391

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 389	. 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  395  anabs1  572  pm4.45  785  unidif0  4197  sucexb  4530  imadmrn  5016  dff1o2  5506  xpsnen  6877  dmaddpq  7441  dmmulpq  7442  eqreznegel  9682  xrnemnf  9846  xrnepnf  9847  elioopnf  10036  elioomnf  10037  elicopnf  10038  elxrge0  10047  dfrp2  10335  isprm2  12258  bj-sucexg  15484