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  7505  1idprl  7676  1idpru  7677  recexprlem1ssl  7719  recexprlem1ssu  7720  msqge0  8662  mulge0  8665  divsubdirap  8754  divdiv32ap  8766  peano2uz  9676  fzoshftral  10333  expdivap  10701  bcval5  10874  redivap  11058  imdivap  11065  absdiflt  11276  absdifle  11277  retanclap  11906  tannegap  11912  lcmgcdeq  12278  isprm3  12313  prmdvdsexpb  12344  dvdsprmpweqnn  12532  mulgaddcomlem  13353  mulginvcom  13355  cnpf2  14551  blres  14778