Theorem a1i4 15327

Description: Add an antecedent to a wff.

Hypothesis

Ref	Expression
a1i4.1	|- (ph -> (ps -> (ch -> ta)))

Assertion

Ref	Expression
a1i4	|- (ph -> (ps -> (ch -> (th -> ta))))

Proof of Theorem a1i4

Step	Hyp	Ref	Expression
1		a1i4.1	. 2 |- (ph -> (ps -> (ch -> ta)))
2		ax-1 4	. 2 |- (ta -> (th -> ta))
3	1, 2	syl8 27	1 |- (ph -> (ps -> (ch -> (th -> ta))))

Syntax hints:   -> wi 3

This theorem is referenced by:  alexsub 15441  isufil2 15565  filssufillem 15570

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

Copyright terms: Public domain