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 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) → 𝜏)

Syntax hints:   → wi 4   ∧ w3a 1009

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 1011

This theorem is referenced by:  syl3an3b  1316  syl3an3br  1319  vtoclgft  2873  ovmpox  6207  ovmpoga  6208  nnanq0  7815  apreim  8921  apsub1  8960  divassap  9010  ltmul2  9176  xleadd1  10256  xltadd2  10258  elfzo  10534  fzodcel  10538  subcn2  12055  mulcn2  12056  ndvdsp1  12677  gcddiv  12774  lcmneg  12830  mulgaddcom  13926  lspsnss  14713  rnglidlrng  14807  neipsm  15178  opnneip  15183  hmeof1o2  15332  blcntrps  15439  blcntr  15440  neibl  15515  blnei  15516  metss  15518  rpcxpsub  15933  cxpcom  15963  rplogbzexp  15979  konigsbergssiedgwpren  16640