Theorem syl3an3 1284

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

Syntax hints:   → wi 4   ∧ w3a 980

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 982

This theorem is referenced by:  syl3an3b  1287  syl3an3br  1290  vtoclgft  2814  ovmpox  6051  ovmpoga  6052  nnanq0  7525  apreim  8630  apsub1  8669  divassap  8717  ltmul2  8883  xleadd1  9950  xltadd2  9952  elfzo  10224  fzodcel  10228  subcn2  11476  mulcn2  11477  ndvdsp1  12097  gcddiv  12186  lcmneg  12242  mulgaddcom  13276  lspsnss  13960  rnglidlrng  14054  neipsm  14390  opnneip  14395  hmeof1o2  14544  blcntrps  14651  blcntr  14652  neibl  14727  blnei  14728  metss  14730  rpcxpsub  15144  cxpcom  15174  rplogbzexp  15190