Theorem sylan9 409

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 ) )

Syntax hints:   -> wi 4   /\ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107

This theorem is referenced by:  sbequi  1887  rspc2  2921  rspc3v  2926  copsexg  4336  chfnrn  5758  ffnfv  5805  f1elima  5914  smoel2  6469  th3q  6809  fiintim  7123  addnnnq0  7669  mulnnnq0  7670  addsrpr  7965  mulsrpr  7966  cau3lem  11692  rescncf  15324