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  11889  mulcn2  11890  ndvdsp1  12511  gcddiv  12608  lcmneg  12664  mulgaddcom  13751  lspsnss  14437  rnglidlrng  14531  neipsm  14897  opnneip  14902  hmeof1o2  15051  blcntrps  15158  blcntr  15159  neibl  15234  blnei  15235  metss  15237  rpcxpsub  15651  cxpcom  15681  rplogbzexp  15697  konigsbergssiedgwpren  16355