Theorem a1i14 15328

Description: Add two antecedents to a wff.

Hypothesis

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

Assertion

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

Proof of Theorem a1i14

Step	Hyp	Ref	Expression
1		a1i14.1	. . 3 |- (ps -> (ch -> ta))
2	1	a1dd 53	. 2 |- (ps -> (ch -> (th -> ta)))
3	2	a1i 8	1 |- (ph -> (ps -> (ch -> (th -> ta))))

Syntax hints:   -> wi 3

This theorem is referenced by:  elfiun 15369

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

Copyright terms: Public domain