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 ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜃) → 𝜏)

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  syl3an2b  1315  syl3an2br  1318  syl3anl2  1327  nndi  6763  nnmass  6764  prarloclemarch2  7792  1idprl  7963  1idpru  7964  recexprlem1ssl  8006  recexprlem1ssu  8007  msqge0  8952  mulge0  8955  divsubdirap  9046  divdiv32ap  9058  peano2uz  9999  fzoshftral  10674  expdivap  11048  bcval5  11223  ccats1val1g  11429  redivap  11661  imdivap  11668  absdiflt  11881  absdifle  11882  retanclap  12514  tannegap  12520  lcmgcdeq  12886  isprm3  12921  prmdvdsexpb  12953  dvdsprmpweqnn  13144  mulgaddcomlem  14007  mulginvcom  14009  cnpf2  15433  blres  15660