Theorem syl3an1 1266

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

Syntax hints:   → wi 4   ∧ w3a 973

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

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

This theorem is referenced by:  syl3an1b  1269  syl3an1br  1272  wepo  4342  f1ofveu  5838  fovrnda  5993  smoiso  6278  tfrcl  6340  omv  6431  oeiv  6432  nndi  6462  nnmsucr  6464  f1oen2g  6729  f1dom2g  6730  undiffi  6898  prarloclemarch2  7368  distrnq0  7408  ltprordil  7538  1idprl  7539  1idpru  7540  ltpopr  7544  ltexprlemopu  7552  ltexprlemdisj  7555  ltexprlemfl  7558  ltexprlemfu  7560  ltexprlemru  7561  recexprlemdisj  7579  recexprlemss1l  7584  recexprlemss1u  7585  cnegexlem1  8081  msqge0  8522  mulge0  8525  divnegap  8610  divdiv32ap  8624  divneg2ap  8640  peano2uz  9529  lbzbi  9562  negqmod0  10274  modqmuladdnn0  10311  expnlbnd  10587  shftfvalg  10769  xrmaxaddlem  11210  retanclap  11672  tannegap  11678  demoivreALT  11723  gcd0id  11921  isprm3  12059  euclemma  12087  phiprmpw  12163  fermltl  12175  mndcl  12646  grpcl  12703  dfgrp2  12719  grprcan  12727  psmetcl  13079  xmetcl  13105  metcl  13106  meteq0  13113  metge0  13119  metsym  13124  blelrnps  13172  blelrn  13173  blssm  13174  blres  13187  mscl  13218  xmscl  13219  xmsge0  13220  xmseq0  13221  xmssym  13222  mopnin  13240  sincosq1sgn  13500  sincosq2sgn  13501  sincosq3sgn  13502  sincosq4sgn  13503  lgsneg1  13679