Theorem syl3an3 1263

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

Syntax hints:   → wi 4   ∧ w3a 968

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116  df-3an 970

This theorem is referenced by:  syl3an3b  1266  syl3an3br  1269  vtoclgft  2776  ovmpox  5970  ovmpoga  5971  nnanq0  7399  apreim  8501  apsub1  8540  divassap  8586  ltmul2  8751  xleadd1  9811  xltadd2  9813  elfzo  10084  fzodcel  10087  subcn2  11252  mulcn2  11253  ndvdsp1  11869  gcddiv  11952  lcmneg  12006  neipsm  12794  opnneip  12799  hmeof1o2  12948  blcntrps  13055  blcntr  13056  neibl  13131  blnei  13132  metss  13134  rpcxpsub  13469  cxpcom  13497  rplogbzexp  13512