Theorem syl3an2 1203

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

Syntax hints:   → wi 4   ∧ w3a 919

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

This theorem depends on definitions:  df-bi 115  df-3an 921

This theorem is referenced by:  syl3an2b  1206  syl3an2br  1209  syl3anl2  1218  nndi  6088  nnmass  6089  prarloclemarch2  6609  1idprl  6780  1idpru  6781  recexprlem1ssl  6823  recexprlem1ssu  6824  msqge0  7716  mulge0  7719  divsubdirap  7796  divdiv32ap  7808  peano2uz  8671  fzoshftral  9247  expdivap  9527  ibcval5  9690  redivap  9761  imdivap  9768  absdiflt  9978  absdifle  9979  lcmgcdeq  10465  isprm3  10500  prmdvdsexpb  10528