Theorem pm4.71

Description: Implication in terms of biconditional and conjunction. Theorem *4.71 of WhiteheadRussell p. 120. (Contributed by NM, 21-Jun-1993) (Proof shortened by Wolf Lammen, 2-Dec-2012)

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

Proof

Step	Hyp	Ref	Expression
1		simpl	|- ( ( ph /\ ps ) -> ph )
2	1	biantru	|- ( ( ph -> ( ph /\ ps ) ) <-> ( ( ph -> ( ph /\ ps ) ) /\ ( ( ph /\ ps ) -> ph ) ) )
3		anclb	|- ( ( ph -> ps ) <-> ( ph -> ( ph /\ ps ) ) )
4		dfbi2	|- ( ( ph <-> ( ph /\ ps ) ) <-> ( ( ph -> ( ph /\ ps ) ) /\ ( ( ph /\ ps ) -> ph ) ) )
5	2 3 4	3bitr4i	|- ( ( ph -> ps ) <-> ( ph <-> ( ph /\ ps ) ) )