Theorem syl3an2 1305

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

Syntax hints:   → wi 4   ∧ w3a 1002

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 1004

This theorem is referenced by:  syl3an2b  1308  syl3an2br  1311  syl3anl2  1320  nndi  6630  nnmass  6631  prarloclemarch2  7602  1idprl  7773  1idpru  7774  recexprlem1ssl  7816  recexprlem1ssu  7817  msqge0  8759  mulge0  8762  divsubdirap  8851  divdiv32ap  8863  peano2uz  9774  fzoshftral  10439  expdivap  10807  bcval5  10980  ccats1val1g  11165  redivap  11380  imdivap  11387  absdiflt  11598  absdifle  11599  retanclap  12228  tannegap  12234  lcmgcdeq  12600  isprm3  12635  prmdvdsexpb  12666  dvdsprmpweqnn  12854  mulgaddcomlem  13677  mulginvcom  13679  cnpf2  14875  blres  15102