Theorem syl3an2 1283

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

Syntax hints:   → wi 4   ∧ w3a 980

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 982

This theorem is referenced by:  syl3an2b  1286  syl3an2br  1289  syl3anl2  1298  nndi  6553  nnmass  6554  prarloclemarch2  7503  1idprl  7674  1idpru  7675  recexprlem1ssl  7717  recexprlem1ssu  7718  msqge0  8660  mulge0  8663  divsubdirap  8752  divdiv32ap  8764  peano2uz  9674  fzoshftral  10331  expdivap  10699  bcval5  10872  redivap  11056  imdivap  11063  absdiflt  11274  absdifle  11275  retanclap  11904  tannegap  11910  lcmgcdeq  12276  isprm3  12311  prmdvdsexpb  12342  dvdsprmpweqnn  12530  mulgaddcomlem  13351  mulginvcom  13353  cnpf2  14527  blres  14754