Theorem dedlem0a 567

Description: Lemma for an alternate version of weak deduction theorem.

Assertion

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

Proof of Theorem dedlem0a

Step	Hyp	Ref	Expression
1		ax-1 3	. . . 4 |- (ps -> ((ch -> ph) -> ps))
2	1	a1i 7	. . 3 |- (ph -> (ps -> ((ch -> ph) -> ps)))
3		ax-1 3	. . . . 5 |- (ph -> (ch -> ph))
4	3	syl4 19	. . . 4 |- (((ch -> ph) -> ps) -> (ph -> ps))
5	4	com12 13	. . 3 |- (ph -> (((ch -> ph) -> ps) -> ps))
6	2, 5	impbid 397	. 2 |- (ph -> (ps <-> ((ch -> ph) -> ps)))
7		iba 486	. . 3 |- (ph -> (ps <-> (ps /\ ph)))
8	7	imbi2d 464	. 2 |- (ph -> (((ch -> ph) -> ps) <-> ((ch -> ph) -> (ps /\ ph))))
9	6, 8	bitrd 406	1 |- (ph -> (ps <-> ((ch -> ph) -> (ps /\ ph))))

Syntax hints:   -> wi 2   <-> wb 127   /\ wa 196

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6

This theorem depends on definitions:  df-bi 128  df-an 198

metamath.org