Theorem syl3an1 1304

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

Syntax hints:   → wi 4   ∧ w3a 1002

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 1004

This theorem is referenced by:  syl3an1b  1307  syl3an1br  1310  wepo  4449  f1ofveu  5988  fovcdmda  6148  smoiso  6446  tfrcl  6508  omv  6599  oeiv  6600  nndi  6630  nnmsucr  6632  f1oen2g  6904  f1dom2g  6905  undiffi  7083  prarloclemarch2  7602  distrnq0  7642  ltprordil  7772  1idprl  7773  1idpru  7774  ltpopr  7778  ltexprlemopu  7786  ltexprlemdisj  7789  ltexprlemfl  7792  ltexprlemfu  7794  ltexprlemru  7795  recexprlemdisj  7813  recexprlemss1l  7818  recexprlemss1u  7819  cnegexlem1  8317  msqge0  8759  mulge0  8762  divnegap  8849  divdiv32ap  8863  divneg2ap  8879  peano2uz  9774  lbzbi  9807  negqmod0  10548  modqmuladdnn0  10585  expnlbnd  10881  fun2dmnop  11065  shftfvalg  11324  xrmaxaddlem  11766  retanclap  12228  tannegap  12234  demoivreALT  12280  gcd0id  12495  isprm3  12635  euclemma  12663  phiprmpw  12739  fermltl  12751  sgrpcl  13437  mndcl  13451  imasmnd2  13480  grpcl  13536  dfgrp2  13555  grprcan  13565  grpsubcl  13608  imasgrp2  13642  mhmid  13647  mhmmnd  13648  mulginvcom  13679  mulgnndir  13683  mulgnnass  13689  qusgrp  13764  ghmmulg  13788  ghmrn  13789  ghmeqker  13803  ablcom  13835  ablinvadd  13842  ghmcmn  13859  rngacl  13900  rngpropd  13913  srgacl  13940  srgcom  13941  ringacl  13988  imasring  14022  subrngacl  14166  subrgacl  14190  subrgugrp  14198  lmodacl  14257  lmodmcl  14258  lmodvacl  14260  lmodvsubcl  14290  lmod4  14295  lmodvaddsub4  14297  lmodvpncan  14298  lmodvnpcan  14299  lmodsubeq0  14304  psmetcl  14994  xmetcl  15020  metcl  15021  meteq0  15028  metge0  15034  metsym  15039  blelrnps  15087  blelrn  15088  blssm  15089  blres  15102  mscl  15133  xmscl  15134  xmsge0  15135  xmseq0  15136  xmssym  15137  mopnin  15155  sincosq1sgn  15494  sincosq2sgn  15495  sincosq3sgn  15496  sincosq4sgn  15497  lgsneg1  15698  usgredg2vtx  16009  uspgredg2vtxeu  16010  usgredg2vtxeu  16011