Theorem syl3an2 1307

Description: A syllogism inference. (Contributed by NM, 22-Aug-1995.)

Hypotheses

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

Assertion

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

Proof of Theorem syl3an2

Step	Hyp	Ref	Expression
1		syl3an2.1	. . 3 ⊢ (𝜑 → 𝜒)
2		syl3an2.2	. . . 4 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)
3	2	3exp 1228	. . 3 ⊢ (𝜓 → (𝜒 → (𝜃 → 𝜏)))
4	1, 3	syl5 32	. 2 ⊢ (𝜓 → (𝜑 → (𝜃 → 𝜏)))
5	4	3imp 1219	1 ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜃) → 𝜏)

Syntax hints:   → wi 4   ∧ w3a 1004

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

This theorem depends on definitions:  df-bi 117  df-3an 1006

This theorem is referenced by:  syl3an2b  1310  syl3an2br  1313  syl3anl2  1322  nndi  6653  nnmass  6654  prarloclemarch2  7638  1idprl  7809  1idpru  7810  recexprlem1ssl  7852  recexprlem1ssu  7853  msqge0  8795  mulge0  8798  divsubdirap  8887  divdiv32ap  8899  peano2uz  9816  fzoshftral  10483  expdivap  10851  bcval5  11024  ccats1val1g  11215  redivap  11434  imdivap  11441  absdiflt  11652  absdifle  11653  retanclap  12282  tannegap  12288  lcmgcdeq  12654  isprm3  12689  prmdvdsexpb  12720  dvdsprmpweqnn  12908  mulgaddcomlem  13731  mulginvcom  13733  cnpf2  14930  blres  15157