Theorem syl3an2 1305

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 1226	. . 3 ⊢ (𝜓 → (𝜒 → (𝜃 → 𝜏)))
4	1, 3	syl5 32	. 2 ⊢ (𝜓 → (𝜑 → (𝜃 → 𝜏)))
5	4	3imp 1217	1 ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜃) → 𝜏)

Syntax hints:   → wi 4   ∧ w3a 1002

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 1004

This theorem is referenced by:  syl3an2b  1308  syl3an2br  1311  syl3anl2  1320  nndi  6640  nnmass  6641  prarloclemarch2  7617  1idprl  7788  1idpru  7789  recexprlem1ssl  7831  recexprlem1ssu  7832  msqge0  8774  mulge0  8777  divsubdirap  8866  divdiv32ap  8878  peano2uz  9790  fzoshftral  10456  expdivap  10824  bcval5  10997  ccats1val1g  11185  redivap  11400  imdivap  11407  absdiflt  11618  absdifle  11619  retanclap  12248  tannegap  12254  lcmgcdeq  12620  isprm3  12655  prmdvdsexpb  12686  dvdsprmpweqnn  12874  mulgaddcomlem  13697  mulginvcom  13699  cnpf2  14896  blres  15123