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  2787  ovmpox  6002  ovmpoga  6003  nnanq0  7456  apreim  8559  apsub1  8598  divassap  8646  ltmul2  8812  xleadd1  9874  xltadd2  9876  elfzo  10148  fzodcel  10151  subcn2  11318  mulcn2  11319  ndvdsp1  11936  gcddiv  12019  lcmneg  12073  mulgaddcom  13005  neipsm  13624  opnneip  13629  hmeof1o2  13778  blcntrps  13885  blcntr  13886  neibl  13961  blnei  13962  metss  13964  rpcxpsub  14299  cxpcom  14327  rplogbzexp  14342