Theorem syl3an3 1273

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

Syntax hints:   → wi 4   ∧ w3a 978

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 980

This theorem is referenced by:  syl3an3b  1276  syl3an3br  1279  vtoclgft  2789  ovmpox  6005  ovmpoga  6006  nnanq0  7459  apreim  8562  apsub1  8601  divassap  8649  ltmul2  8815  xleadd1  9877  xltadd2  9879  elfzo  10151  fzodcel  10154  subcn2  11321  mulcn2  11322  ndvdsp1  11939  gcddiv  12022  lcmneg  12076  mulgaddcom  13012  neipsm  13693  opnneip  13698  hmeof1o2  13847  blcntrps  13954  blcntr  13955  neibl  14030  blnei  14031  metss  14033  rpcxpsub  14368  cxpcom  14396  rplogbzexp  14411