Theorem 3ax5 5832

Description: ax-5 1302 for a 3 element left-nested implication. Derived automatically from 3ax5VD 16686. (Contributed by Alan Sare, 31-Dec-2011.)

Assertion

Ref	Expression
3ax5	|- (A.x(ph -> (ps -> ch)) -> (A.xph -> (A.xps -> A.xch)))

Proof of Theorem 3ax5

Step	Hyp	Ref	Expression
1		ax-5 1302	. 2 |- (A.x(ph -> (ps -> ch)) -> (A.xph -> A.x(ps -> ch)))
2		ax-5 1302	. 2 |- (A.x(ps -> ch) -> (A.xps -> A.xch))
3	1, 2	syl6 25	1 |- (A.x(ph -> (ps -> ch)) -> (A.xph -> (A.xps -> A.xch)))

Syntax hints:   -> wi 3  A.wal 1296

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-mp 7  ax-5 1302

Copyright terms: Public domain