Theorem syl3an3 1284

Description: A syllogism inference. (Contributed by NM, 22-Aug-1995.)

Hypotheses

Ref	Expression
syl3an3.1	⊢ (𝜑 → 𝜃)
syl3an3.2	⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)

Assertion

Ref	Expression
syl3an3	⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) → 𝜏)

Proof of Theorem syl3an3

Step	Hyp	Ref	Expression
1		syl3an3.1	. . 3 ⊢ (𝜑 → 𝜃)
2		syl3an3.2	. . . 4 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)
3	2	3exp 1204	. . 3 ⊢ (𝜓 → (𝜒 → (𝜃 → 𝜏)))
4	1, 3	syl7 69	. 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:  syl3an3b  1287  syl3an3br  1290  vtoclgft  2810  ovmpox  6047  ovmpoga  6048  nnanq0  7518  apreim  8622  apsub1  8661  divassap  8709  ltmul2  8875  xleadd1  9941  xltadd2  9943  elfzo  10215  fzodcel  10219  subcn2  11454  mulcn2  11455  ndvdsp1  12073  gcddiv  12156  lcmneg  12212  mulgaddcom  13216  lspsnss  13900  rnglidlrng  13994  neipsm  14322  opnneip  14327  hmeof1o2  14476  blcntrps  14583  blcntr  14584  neibl  14659  blnei  14660  metss  14662  rpcxpsub  15043  cxpcom  15071  rplogbzexp  15086