Theorem sylan9 508

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

Hypotheses

Ref	Expression
sylan9.1	⊢ (𝜑 → (𝜓 → 𝜒))
sylan9.2	⊢ (𝜃 → (𝜒 → 𝜏))

Assertion

Ref	Expression
sylan9	⊢ ((𝜑 ∧ 𝜃) → (𝜓 → 𝜏))

Proof of Theorem sylan9

Step	Hyp	Ref	Expression
1		sylan9.1	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
2		sylan9.2	. . 3 ⊢ (𝜃 → (𝜒 → 𝜏))
3	1, 2	syl9 77	. 2 ⊢ (𝜑 → (𝜃 → (𝜓 → 𝜏)))
4	3	imp 407	1 ⊢ ((𝜑 ∧ 𝜃) → (𝜓 → 𝜏))

Syntax hints:   → wi 4   ∧ wa 396

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

This theorem depends on definitions:  df-bi 206  df-an 397

This theorem is referenced by:  ax8  2112  ax9  2120  rspc2  3589  rspc2v  3591  rspc3v  3594  rspc4v  3596  rspc8v  3597  copsexgw  5452  copsexg  5453  chfnrn  7004  fvcofneq  7048  ffnfv  7071  f1elima  7215  onint  7730  peano5  7835  peano5OLD  7836  f1oweALT  7910  smoel2  8314  pssnn  9119  php  9161  pssnnOLD  9216  fiint  9275  dffi2  9368  alephnbtwn  10016  cfcof  10219  zorn2lem7  10447  suplem1pr  10997  addsrpr  11020  mulsrpr  11021  cau3lem  15251  divalglem8  16293  efgi  19515  elfrlmbasn0  21206  locfincmp  22914  tx1stc  23038  fbunfip  23257  filuni  23273  ufileu  23307  rescncf  24297  shmodsi  30394  spanuni  30549  spansneleq  30575  mdi  31300  dmdi  31307  dmdi4  31312  funimass4f  31618  bj-ax89  35218  poimirlem32  36183  ffnafv  45523