Theorem syl3an3 1308

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

Syntax hints:   → wi 4   ∧ w3a 1004

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 1006

This theorem is referenced by:  syl3an3b  1311  syl3an3br  1314  vtoclgft  2854  ovmpox  6150  ovmpoga  6151  nnanq0  7678  apreim  8783  apsub1  8822  divassap  8870  ltmul2  9036  xleadd1  10110  xltadd2  10112  elfzo  10384  fzodcel  10388  subcn2  11876  mulcn2  11877  ndvdsp1  12498  gcddiv  12595  lcmneg  12651  mulgaddcom  13738  lspsnss  14424  rnglidlrng  14518  neipsm  14884  opnneip  14889  hmeof1o2  15038  blcntrps  15145  blcntr  15146  neibl  15221  blnei  15222  metss  15224  rpcxpsub  15638  cxpcom  15668  rplogbzexp  15684