Theorem sylan9 511

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

Syntax hints:   → wi 4   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  ax8  2117  ax9  2125  rspc2  3549  rspc2v  3551  rspc3v  3554  copsexgw  5349  copsexg  5350  chfnrn  6810  fvcofneq  6850  ffnfv  6873  f1elima  7013  onint  7509  peano5  7604  f1oweALT  7677  smoel2  8010  pssnn  8738  pssnnOLD  8774  fiint  8828  dffi2  8920  alephnbtwn  9531  cfcof  9734  zorn2lem7  9962  suplem1pr  10512  addsrpr  10535  mulsrpr  10536  cau3lem  14762  divalglem8  15801  efgi  18912  elfrlmbasn0  20528  locfincmp  22226  tx1stc  22350  fbunfip  22569  filuni  22585  ufileu  22619  rescncf  23598  shmodsi  29271  spanuni  29426  spansneleq  29452  mdi  30177  dmdi  30184  dmdi4  30189  funimass4f  30494  bj-ax89  34405  poimirlem32  35369  ffnafv  44095