Theorem dedlem0a

Description: Lemma for an alternate version of weak deduction theorem. (Contributed by NM, 2-Apr-1994) (Proof shortened by Andrew Salmon, 7-May-2011) (Proof shortened by Wolf Lammen, 4-Dec-2012)

	Ref	Expression
Assertion	dedlem0a	|- ( ph -> ( ps <-> ( ( ch -> ph ) -> ( ps /\ ph ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		iba	|- ( ph -> ( ps <-> ( ps /\ ph ) ) )
2		biimt	|- ( ( ch -> ph ) -> ( ( ps /\ ph ) <-> ( ( ch -> ph ) -> ( ps /\ ph ) ) ) )
3	2	jarri	|- ( ph -> ( ( ps /\ ph ) <-> ( ( ch -> ph ) -> ( ps /\ ph ) ) ) )
4	1 3	bitrd	|- ( ph -> ( ps <-> ( ( ch -> ph ) -> ( ps /\ ph ) ) ) )