Theorem syl3an3 1252

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 1181	. . 3 ⊢ (𝜓 → (𝜒 → (𝜃 → 𝜏)))
4	1, 3	syl7 69	. 2 ⊢ (𝜓 → (𝜒 → (𝜑 → 𝜏)))
5	4	3imp 1176	1 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) → 𝜏)

Syntax hints:   → wi 4   ∧ w3a 963

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116  df-3an 965

This theorem is referenced by:  syl3an3b  1255  syl3an3br  1258  vtoclgft  2739  ovmpox  5907  ovmpoga  5908  nnanq0  7290  apreim  8389  apsub1  8428  divassap  8474  ltmul2  8638  xleadd1  9688  xltadd2  9690  elfzo  9957  fzodcel  9960  subcn2  11112  mulcn2  11113  ndvdsp1  11665  gcddiv  11743  lcmneg  11791  neipsm  12362  opnneip  12367  hmeof1o2  12516  blcntrps  12623  blcntr  12624  neibl  12699  blnei  12700  metss  12702  rpcxpsub  13037  cxpcom  13065  rplogbzexp  13079