Theorem syl3an2 1250

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

Syntax hints:   → wi 4   ∧ w3a 962

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 964

This theorem is referenced by:  syl3an2b  1253  syl3an2br  1256  syl3anl2  1265  nndi  6382  nnmass  6383  prarloclemarch2  7227  1idprl  7398  1idpru  7399  recexprlem1ssl  7441  recexprlem1ssu  7442  msqge0  8378  mulge0  8381  divsubdirap  8468  divdiv32ap  8480  peano2uz  9378  fzoshftral  10015  expdivap  10344  bcval5  10509  redivap  10646  imdivap  10653  absdiflt  10864  absdifle  10865  retanclap  11429  tannegap  11435  lcmgcdeq  11764  isprm3  11799  prmdvdsexpb  11827  cnpf2  12376  blres  12603