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  6732  nnmass  6733  prarloclemarch2  7750  1idprl  7921  1idpru  7922  recexprlem1ssl  7964  recexprlem1ssu  7965  msqge0  8907  mulge0  8910  divsubdirap  8999  divdiv32ap  9011  peano2uz  9933  fzoshftral  10606  expdivap  10976  bcval5  11150  ccats1val1g  11352  redivap  11584  imdivap  11591  absdiflt  11802  absdifle  11803  retanclap  12433  tannegap  12439  lcmgcdeq  12805  isprm3  12840  prmdvdsexpb  12871  dvdsprmpweqnn  13059  mulgaddcomlem  13898  mulginvcom  13900  cnpf2  15198  blres  15425