Theorem syl3an3 1313

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  syl3an3b  1316  syl3an3br  1319  vtoclgft  2873  ovmpox  6220  ovmpoga  6221  nnanq0  7831  apreim  8939  apsub1  8978  divassap  9028  ltmul2  9194  ind0  9310  xleadd1  10294  xltadd2  10296  elfzo  10573  fzodcel  10577  subcn2  12102  mulcn2  12103  ndvdsp1  12724  gcddiv  12821  lcmneg  12877  mulgaddcom  14008  lspsnss  14850  rnglidlrng  14944  neipsm  15380  opnneip  15385  hmeof1o2  15534  blcntrps  15641  blcntr  15642  neibl  15717  blnei  15718  metss  15720  rpcxpsub  16141  cxpcom  16173  rplogbzexp  16190  konigsbergssiedgwpren  16931