Theorem sylan9 413

Description: Nested syllogism inference conjoining dissimilar antecedents. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 7-May-2011.)

Hypotheses

Ref	Expression
sylan9.1	|- ( ph -> ( ps -> ch ) )
sylan9.2	|- ( th -> ( ch -> ta ) )

Assertion

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

Proof of Theorem sylan9

Step	Hyp	Ref	Expression
1		sylan9.1	. . 3 |- ( ph -> ( ps -> ch ) )
2		sylan9.2	. . 3 |- ( th -> ( ch -> ta ) )
3	1, 2	syl9 72	. 2 |- ( ph -> ( th -> ( ps -> ta ) ) )
4	3	imp 124	1 |- ( ( ph /\ th ) -> ( ps -> ta ) )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107

This theorem is used by:  sbequi  1892  rspc2  2941  rspc3v  2946  copsexg  4386  chfnrn  5823  ffnfv  5869  f1elima  5982  funimass4f  6363  smoel2  6578  th3q  6918  fiintim  7242  addnnnq0  7822  mulnnnq0  7823  addsrpr  8118  mulsrpr  8119  cau3lem  11903  rescncf  15807