Theorem sylan9 359

Description: Nested syllogism inference conjoining dissimilar antecedents.

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	1	adantr 306	. 2 |- ((ph /\ th) -> (ps -> ch))
3		sylan9.2	. . 3 |- (th -> (ch -> ta ))
4	3	adantl 305	. 2 |- ((ph /\ th) -> (ch -> ta ))
5	2, 4	syld 27	1 |- ((ph /\ th) -> (ps -> ta ))

Syntax hints:   -> wi 2   /\ wa 196

This theorem is referenced by:  sbequi 876  sbal1 996  onfr 2237  onint 2261  limom 2387  peano5 2394  chfnrn 2885  ffnfv 2892  isocnv 2934  isotr 2935  isotrALT 2936  f1oweOLD 2944  th3q 3253  pssnn 3428  fiint 3445  r1tr 3498  zornlem7 3609  alephnbtwn 3674  axacndlem4 3756  axacnd 3758  suppsr2 4017  shmods 5363  spanun 5450  spansneleq 5475

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

This theorem depends on definitions:  df-bi 128  df-an 198

metamath.org