Theorem syl3an3 1251

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

Syntax hints:   → wi 4   ∧ w3a 962

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 964

This theorem is referenced by:  syl3an3b  1254  syl3an3br  1257  vtoclgft  2736  ovmpox  5899  ovmpoga  5900  nnanq0  7266  apreim  8365  apsub1  8404  divassap  8450  ltmul2  8614  xleadd1  9658  xltadd2  9660  elfzo  9926  fzodcel  9929  subcn2  11080  mulcn2  11081  ndvdsp1  11629  gcddiv  11707  lcmneg  11755  neipsm  12323  opnneip  12328  hmeof1o2  12477  blcntrps  12584  blcntr  12585  neibl  12660  blnei  12661  metss  12663