Theorem syl3an1 1203

Description: A syllogism inference. (Contributed by NM, 22-Aug-1995.)

Hypotheses

Ref	Expression
syl3an1.1	⊢ (𝜑 → 𝜓)
syl3an1.2	⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)

Assertion

Ref	Expression
syl3an1	⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜏)

Proof of Theorem syl3an1

Step	Hyp	Ref	Expression
1		syl3an1.1	. . 3 ⊢ (𝜑 → 𝜓)
2	1	3anim1i 1125	. 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → (𝜓 ∧ 𝜒 ∧ 𝜃))
3		syl3an1.2	. 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)
4	2, 3	syl 14	1 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜏)

Syntax hints:   → wi 4   ∧ w3a 920

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

This theorem depends on definitions:  df-bi 115  df-3an 922

This theorem is referenced by:  syl3an1b  1206  syl3an1br  1209  wepo  4122  f1ofveu  5531  fovrnda  5675  smoiso  5951  tfrcl  6013  omv  6099  oeiv  6100  nndi  6130  nnmsucr  6132  f1oen2g  6302  f1dom2g  6303  prarloclemarch2  6671  distrnq0  6711  ltprordil  6841  1idprl  6842  1idpru  6843  ltpopr  6847  ltexprlemopu  6855  ltexprlemdisj  6858  ltexprlemfl  6861  ltexprlemfu  6863  ltexprlemru  6864  recexprlemdisj  6882  recexprlemss1l  6887  recexprlemss1u  6888  cnegexlem1  7350  msqge0  7783  mulge0  7786  divnegap  7861  divdiv32ap  7875  divneg2ap  7891  peano2uz  8752  lbzbi  8782  negqmod0  9413  modqmuladdnn0  9450  expnlbnd  9694  shftfvalg  9844  gcd0id  10514  isprm3  10644  euclemma  10669