Theorem a1ddd 76

Description: Triple deduction introducing an antecedent to a wff. Deduction associated with a1dd 47. Double deduction associated with a1d 26. Triple deduction associated with ax-1 6 and a1i 11. (Contributed by Jeff Hankins, 4-Aug-2009.)

Hypothesis

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

Assertion

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

Proof of Theorem a1ddd

Step	Hyp	Ref	Expression
1		a1ddd.1	. 2 |- ( ph -> ( ps -> ( ch -> ta ) ) )
2		ax-1 6	. 2 |- ( ta -> ( th -> ta ) )
3	1, 2	syl8 72	1 |- ( ph -> ( ps -> ( ch -> ( th -> ta ) ) ) )

Syntax hints:   -> wi 4

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

This theorem is referenced by:  ad4ant123  1244  ad5ant13  1251  ad5ant14  1252  ad5ant15  1253  ad5ant23  1254  ad5ant24  1255  ad5ant25  1256  ad5ant245  1257  ad5ant234  1258  ad5ant235  1259  ad5ant123  1260  ad5ant124  1261  ad5ant125  1262  ad5ant134  1263  ad5ant135  1264  ad5ant145  1265