Theorem elimant 505

Description: Elimination of antecedents in an implication.

Assertion

Ref	Expression
elimant	|- (((ph -> ps) /\ ((ps -> ch) -> (ph -> th))) -> (ph -> (ch -> th)))

Proof of Theorem elimant

Step	Hyp	Ref	Expression
1		id 9	. . . . . . . . . . 11 |- ((ph -> ps) -> (ph -> ps))
2	1	impac 304	. . . . . . . . . 10 |- (((ph -> ps) /\ ph) -> (ps /\ ph))
3		pm5.1 501	. . . . . . . . . 10 |- ((ps /\ ph) -> (ps <-> ph))
4	2, 3	syl 12	. . . . . . . . 9 |- (((ph -> ps) /\ ph) -> (ps <-> ph))
5	4	imbi1d 465	. . . . . . . 8 |- (((ph -> ps) /\ ph) -> ((ps -> ch) <-> (ph -> ch)))
6	5	imbi1d 465	. . . . . . 7 |- (((ph -> ps) /\ ph) -> (((ps -> ch) -> (ph -> th)) <-> ((ph -> ch) -> (ph -> th))))
7	6	biimpd 135	. . . . . 6 |- (((ph -> ps) /\ ph) -> (((ps -> ch) -> (ph -> th)) -> ((ph -> ch) -> (ph -> th))))
8	7	exp 291	. . . . 5 |- ((ph -> ps) -> (ph -> (((ps -> ch) -> (ph -> th)) -> ((ph -> ch) -> (ph -> th)))))
9	8	com23 32	. . . 4 |- ((ph -> ps) -> (((ps -> ch) -> (ph -> th)) -> (ph -> ((ph -> ch) -> (ph -> th)))))
10	9	imp 277	. . 3 |- (((ph -> ps) /\ ((ps -> ch) -> (ph -> th))) -> (ph -> ((ph -> ch) -> (ph -> th))))
11		imdi 147	. . 3 |- ((ph -> (ch -> th)) <-> ((ph -> ch) -> (ph -> th)))
12	10, 11	syl6ibr 186	. 2 |- (((ph -> ps) /\ ((ps -> ch) -> (ph -> th))) -> (ph -> (ph -> (ch -> th))))
13	12	pm2.43d 59	1 |- (((ph -> ps) /\ ((ps -> ch) -> (ph -> th))) -> (ph -> (ch -> th)))

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