Theorem syl3an2 1251

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

Syntax hints:   → wi 4   ∧ w3a 963

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

This theorem depends on definitions:  df-bi 116  df-3an 965

This theorem is referenced by:  syl3an2b  1254  syl3an2br  1257  syl3anl2  1266  nndi  6390  nnmass  6391  prarloclemarch2  7251  1idprl  7422  1idpru  7423  recexprlem1ssl  7465  recexprlem1ssu  7466  msqge0  8402  mulge0  8405  divsubdirap  8492  divdiv32ap  8504  peano2uz  9405  fzoshftral  10046  expdivap  10375  bcval5  10541  redivap  10678  imdivap  10685  absdiflt  10896  absdifle  10897  retanclap  11465  tannegap  11471  lcmgcdeq  11800  isprm3  11835  prmdvdsexpb  11863  cnpf2  12415  blres  12642