Theorem sylan9 406

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 123	1 |- ( ( ph /\ th ) -> ( ps -> ta ) )

Syntax hints:   -> wi 4   /\ wa 103

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

This theorem is referenced by:  sbequi  1811  rspc2  2795  rspc3v  2800  copsexg  4161  chfnrn  5524  ffnfv  5571  f1elima  5667  smoel2  6193  th3q  6527  fiintim  6810  addnnnq0  7250  mulnnnq0  7251  addsrpr  7546  mulsrpr  7547  cau3lem  10879  rescncf  12726