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  2814  ovmpox  6052  ovmpoga  6053  nnanq0  7527  apreim  8632  apsub1  8671  divassap  8719  ltmul2  8885  xleadd1  9952  xltadd2  9954  elfzo  10226  fzodcel  10230  subcn2  11478  mulcn2  11479  ndvdsp1  12099  gcddiv  12196  lcmneg  12252  mulgaddcom  13286  lspsnss  13970  rnglidlrng  14064  neipsm  14400  opnneip  14405  hmeof1o2  14554  blcntrps  14661  blcntr  14662  neibl  14737  blnei  14738  metss  14740  rpcxpsub  15154  cxpcom  15184  rplogbzexp  15200