Theorem syl3an1 1214

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 1132	. 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → (𝜓 ∧ 𝜒 ∧ 𝜃))
3		syl3an1.2	. 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)
4	2, 3	syl 14	1 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜏)

Syntax hints:   → wi 4   ∧ w3a 927

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

This theorem depends on definitions:  df-bi 116  df-3an 929

This theorem is referenced by:  syl3an1b  1217  syl3an1br  1220  wepo  4210  f1ofveu  5678  fovrnda  5826  smoiso  6105  tfrcl  6167  omv  6256  oeiv  6257  nndi  6287  nnmsucr  6289  f1oen2g  6552  f1dom2g  6553  undiffi  6715  prarloclemarch2  7075  distrnq0  7115  ltprordil  7245  1idprl  7246  1idpru  7247  ltpopr  7251  ltexprlemopu  7259  ltexprlemdisj  7262  ltexprlemfl  7265  ltexprlemfu  7267  ltexprlemru  7268  recexprlemdisj  7286  recexprlemss1l  7291  recexprlemss1u  7292  cnegexlem1  7754  msqge0  8190  mulge0  8193  divnegap  8270  divdiv32ap  8284  divneg2ap  8300  peano2uz  9170  lbzbi  9200  negqmod0  9887  modqmuladdnn0  9924  expnlbnd  10209  shftfvalg  10383  xrmaxaddlem  10819  retanclap  11177  tannegap  11183  demoivreALT  11227  gcd0id  11412  isprm3  11542  euclemma  11567  phiprmpw  11640  psmetcl  12127  xmetcl  12153  metcl  12154  meteq0  12161  metge0  12167  metsym  12172  blelrnps  12220  blelrn  12221  blssm  12222  blres  12235  mscl  12266  xmscl  12267  xmsge0  12268  xmseq0  12269  xmssym  12270  mopnin  12288