Theorem sylan9 690

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 444	1 ⊢ ((𝜑 ∧ 𝜃) → (𝜓 → 𝜏))

Syntax hints:   → wi 4   ∧ wa 383

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 197  df-an 385

This theorem is referenced by:  ax8  2036  ax9  2043  rspc2  3351  rspc3v  3356  trintssOLD  4803  copsexg  4985  chfnrn  6368  fvcofneq  6407  ffnfv  6428  f1elima  6560  onint  7037  peano5  7131  f1oweALT  7194  smoel2  7505  pssnn  8219  fiint  8278  dffi2  8370  alephnbtwn  8932  cfcof  9134  zorn2lem7  9362  suplem1pr  9912  addsrpr  9934  mulsrpr  9935  cau3lem  14138  divalglem8  15170  efgi  18178  elfrlmbasn0  20154  locfincmp  21377  tx1stc  21501  fbunfip  21720  filuni  21736  ufileu  21770  rescncf  22747  shmodsi  28376  spanuni  28531  spansneleq  28557  mdi  29282  dmdi  29289  dmdi4  29294  funimass4f  29565  bj-ax89  32792  wl-ax8clv1  33508  wl-ax8clv2  33511  poimirlem32  33571  ffnafv  41572