Theorem syl3an2 1284

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

Syntax hints:   → wi 4   ∧ w3a 981

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 983

This theorem is referenced by:  syl3an2b  1287  syl3an2br  1290  syl3anl2  1299  nndi  6584  nnmass  6585  prarloclemarch2  7547  1idprl  7718  1idpru  7719  recexprlem1ssl  7761  recexprlem1ssu  7762  msqge0  8704  mulge0  8707  divsubdirap  8796  divdiv32ap  8808  peano2uz  9719  fzoshftral  10384  expdivap  10752  bcval5  10925  ccats1val1g  11109  redivap  11255  imdivap  11262  absdiflt  11473  absdifle  11474  retanclap  12103  tannegap  12109  lcmgcdeq  12475  isprm3  12510  prmdvdsexpb  12541  dvdsprmpweqnn  12729  mulgaddcomlem  13551  mulginvcom  13553  cnpf2  14749  blres  14976