Theorem syl3an2 1308

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

Syntax hints:   → wi 4   ∧ w3a 1005

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 1007

This theorem is referenced by:  syl3an2b  1311  syl3an2br  1314  syl3anl2  1323  nndi  6697  nnmass  6698  prarloclemarch2  7682  1idprl  7853  1idpru  7854  recexprlem1ssl  7896  recexprlem1ssu  7897  msqge0  8838  mulge0  8841  divsubdirap  8930  divdiv32ap  8942  peano2uz  9861  fzoshftral  10530  expdivap  10898  bcval5  11071  ccats1val1g  11265  redivap  11497  imdivap  11504  absdiflt  11715  absdifle  11716  retanclap  12346  tannegap  12352  lcmgcdeq  12718  isprm3  12753  prmdvdsexpb  12784  dvdsprmpweqnn  12972  mulgaddcomlem  13795  mulginvcom  13797  cnpf2  15001  blres  15228