Theorem syland 498

Description: A syllogism deduction. (Contributed by NM, 15-Dec-2004.)

Hypotheses

Ref	Expression
syland.1	|- ( ph -> ( ps -> ch ) )
syland.2	|- ( ph -> ( ( ch /\ th ) -> ta ) )

Assertion

Ref	Expression
syland	|- ( ph -> ( ( ps /\ th ) -> ta ) )

Proof of Theorem syland

Step	Hyp	Ref	Expression
1		syland.1	. . 3 |- ( ph -> ( ps -> ch ) )
2		syland.2	. . . 4 |- ( ph -> ( ( ch /\ th ) -> ta ) )
3	2	expd 452	. . 3 |- ( ph -> ( ch -> ( th -> ta ) ) )
4	1, 3	syld 47	. 2 |- ( ph -> ( ps -> ( th -> ta ) ) )
5	4	impd 447	1 |- ( ph -> ( ( ps /\ th ) -> ta ) )

Syntax hints:   -> wi 4   /\ wa 384

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

This theorem depends on definitions:  df-bi 197  df-an 386

This theorem is referenced by:  sylan2d  499  syl2and  500  sylani  686  onfununi  7438  lt2add  10513  nn0seqcvgd  15283  1stcelcls  21264  llyidm  21291  filuni  21689  ballotlemimin  30567  btwnintr  32126  ifscgr  32151  btwnconn1lem12  32205  poimir  33442  cvrntr  34711  goldbachthlem2  41458