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  4384  chfnrn  5820  ffnfv  5866  f1elima  5979  funimass4f  6359  smoel2  6574  th3q  6914  fiintim  7238  addnnnq0  7816  mulnnnq0  7817  addsrpr  8112  mulsrpr  8113  cau3lem  11880  rescncf  15682