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  6149  ovmpoga  6150  nnanq0  7677  apreim  8782  apsub1  8821  divassap  8869  ltmul2  9035  xleadd1  10109  xltadd2  10111  elfzo  10383  fzodcel  10387  subcn2  11871  mulcn2  11872  ndvdsp1  12492  gcddiv  12589  lcmneg  12645  mulgaddcom  13732  lspsnss  14417  rnglidlrng  14511  neipsm  14877  opnneip  14882  hmeof1o2  15031  blcntrps  15138  blcntr  15139  neibl  15214  blnei  15215  metss  15217  rpcxpsub  15631  cxpcom  15661  rplogbzexp  15677