Theorem syl3an2 1312

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

Syntax hints:   → wi 4   ∧ w3a 1009

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 1011

This theorem is referenced by:  syl3an2b  1315  syl3an2br  1318  syl3anl2  1327  nndi  6749  nnmass  6750  prarloclemarch2  7776  1idprl  7947  1idpru  7948  recexprlem1ssl  7990  recexprlem1ssu  7991  msqge0  8934  mulge0  8937  divsubdirap  9028  divdiv32ap  9040  peano2uz  9962  fzoshftral  10635  expdivap  11005  bcval5  11179  ccats1val1g  11385  redivap  11617  imdivap  11624  absdiflt  11836  absdifle  11837  retanclap  12467  tannegap  12473  lcmgcdeq  12839  isprm3  12874  prmdvdsexpb  12905  dvdsprmpweqnn  13093  mulgaddcomlem  13925  mulginvcom  13927  cnpf2  15231  blres  15458