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  4454  f1ofveu  6001  fovcdmda  6161  smoiso  6463  tfrcl  6525  omv  6618  oeiv  6619  nndi  6649  nnmsucr  6651  f1oen2g  6923  f1dom2g  6924  undiffi  7110  prarloclemarch2  7629  distrnq0  7669  ltprordil  7799  1idprl  7800  1idpru  7801  ltpopr  7805  ltexprlemopu  7813  ltexprlemdisj  7816  ltexprlemfl  7819  ltexprlemfu  7821  ltexprlemru  7822  recexprlemdisj  7840  recexprlemss1l  7845  recexprlemss1u  7846  cnegexlem1  8344  msqge0  8786  mulge0  8789  divnegap  8876  divdiv32ap  8890  divneg2ap  8906  peano2uz  9807  lbzbi  9840  negqmod0  10583  modqmuladdnn0  10620  expnlbnd  10916  fun2dmnop  11102  shftfvalg  11369  xrmaxaddlem  11811  retanclap  12273  tannegap  12279  demoivreALT  12325  gcd0id  12540  isprm3  12680  euclemma  12708  phiprmpw  12784  fermltl  12796  sgrpcl  13482  mndcl  13496  imasmnd2  13525  grpcl  13581  dfgrp2  13600  grprcan  13610  grpsubcl  13653  imasgrp2  13687  mhmid  13692  mhmmnd  13693  mulginvcom  13724  mulgnndir  13728  mulgnnass  13734  qusgrp  13809  ghmmulg  13833  ghmrn  13834  ghmeqker  13848  ablcom  13880  ablinvadd  13887  ghmcmn  13904  rngacl  13945  rngpropd  13958  srgacl  13985  srgcom  13986  ringacl  14033  imasring  14067  subrngacl  14212  subrgacl  14236  subrgugrp  14244  lmodacl  14303  lmodmcl  14304  lmodvacl  14306  lmodvsubcl  14336  lmod4  14341  lmodvaddsub4  14343  lmodvpncan  14344  lmodvnpcan  14345  lmodsubeq0  14350  psmetcl  15040  xmetcl  15066  metcl  15067  meteq0  15074  metge0  15080  metsym  15085  blelrnps  15133  blelrn  15134  blssm  15135  blres  15148  mscl  15179  xmscl  15180  xmsge0  15181  xmseq0  15182  xmssym  15183  mopnin  15201  sincosq1sgn  15540  sincosq2sgn  15541  sincosq3sgn  15542  sincosq4sgn  15543  lgsneg1  15744  usgredg2vtx  16056  uspgredg2vtxeu  16057  usgredg2vtxeu  16058