Theorem syl3an3 1306

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

Syntax hints:   → wi 4   ∧ w3a 1002

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 1004

This theorem is referenced by:  syl3an3b  1309  syl3an3br  1312  vtoclgft  2852  ovmpox  6145  ovmpoga  6146  nnanq0  7668  apreim  8773  apsub1  8812  divassap  8860  ltmul2  9026  xleadd1  10100  xltadd2  10102  elfzo  10374  fzodcel  10378  subcn2  11862  mulcn2  11863  ndvdsp1  12483  gcddiv  12580  lcmneg  12636  mulgaddcom  13723  lspsnss  14408  rnglidlrng  14502  neipsm  14868  opnneip  14873  hmeof1o2  15022  blcntrps  15129  blcntr  15130  neibl  15205  blnei  15206  metss  15208  rpcxpsub  15622  cxpcom  15652  rplogbzexp  15668