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  786  unidif0  4212  sucexb  4546  imadmrn  5033  dff1o2  5529  xpsnen  6918  dmaddpq  7494  dmmulpq  7495  eqreznegel  9737  xrnemnf  9901  xrnepnf  9902  elioopnf  10091  elioomnf  10092  elicopnf  10093  elxrge0  10102  dfrp2  10408  isprm2  12472  bj-sucexg  15895