Theorem syl3an1 1161

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

Syntax hints:   → wi 4   ∧ w3a 1085

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 206  df-an 396  df-3an 1087

This theorem is referenced by:  3adant1l  1174  3adant1r  1175  syl3an1b  1401  syl3an1br  1404  wefrc  5574  tz7.5  6272  f1ofvswap  7158  f1ofveu  7250  fovrnda  7421  suppvalfng  7955  smoiso  8164  odi  8372  nndi  8416  nnmsucr  8418  f1oen2g  8711  f1dom2g  8712  f1dom2gOLD  8713  domssex2  8873  enfii  8932  ordunifi  8994  ackbij1lem16  9922  divneg  11597  divdiv32  11613  divneg2  11629  ltdiv2  11791  fimaxre  11849  fiminre  11852  suprzcl  12330  peano2uz  12570  infssuzle  12600  lbzbi  12605  zbtwnre  12615  irrmul  12643  supxrunb1  12982  expnlbnd  13876  hash1to3  14133  fun2dmnop  14137  brfi1uzind  14140  brcnvtrclfvcnv  14644  retancl  15779  tanneg  15785  demoivreALT  15838  dvdscmulr  15922  dvdsmulcr  15923  mulmoddvds  15967  gcd0id  16154  euclemma  16346  phiprmpw  16405  fermltl  16413  vdwapun  16603  vdwapid1  16604  cshwshashlem1  16725  fsets  16798  pospo  17978  tltnle  18055  latasymb  18075  mndcl  18308  imasmnd2  18337  gsumsgrpccat  18393  grpcl  18500  dfgrp2  18519  grprcan  18528  grpsubcl  18570  imasgrp2  18605  mhmid  18611  mhmmnd  18612  mulginvcom  18643  mulgnndir  18647  mulgnnass  18653  qusgrp  18726  ghmmulg  18761  ghmrn  18762  ghmeqker  18776  gsumccatsymgsn  18949  ablcom  19319  ablinvadd  19326  mulgmhm  19344  mulgghm  19345  ghmcmn  19348  odadd1  19364  odadd2  19365  srgcl  19663  srgacl  19675  srgcom  19676  ringcl  19715  crngcom  19716  ringacl  19732  imasring  19773  irredlmul  19865  rhmmul  19886  drngmcl  19919  isdrngd  19931  subrgacl  19950  subrgugrp  19958  srngadd  20032  srngmul  20033  idsrngd  20037  lmodacl  20049  lmodmcl  20050  lmodvacl  20052  lmodvsubcl  20083  lmod4  20088  lmodvaddsub4  20090  lmodvpncan  20091  lmodvnpcan  20092  lmodsubeq0  20097  pwssplit3  20238  islbs2  20331  islbs3  20332  lbsext  20340  rspssp  20410  zlmlmod  20640  psgnco  20700  ipdir  20756  ip2eq  20770  ocvin  20791  frlmsplit2  20890  ascldimul  21002  rnasclmulcl  21008  mplbas2  21153  coe1add  21345  coe1subfv  21347  coe1mul2  21350  ringvcl  21457  cramer  21748  chpmat1d  21893  filin  22913  filfinnfr  22936  filuni  22944  ufprim  22968  uffinfix  22986  hausflf  23056  uffcfflf  23098  cnextcn  23126  tmdmulg  23151  tsmsxplem1  23212  psmetcl  23368  xmetcl  23392  metcl  23393  meteq0  23400  metge0  23406  metsym  23411  metgt0  23420  blelrnps  23477  blelrn  23478  blssm  23479  blres  23492  mscl  23522  xmscl  23523  xmsge0  23524  xmseq0  23525  xmssym  23526  mopnin  23559  nmf2  23655  ngpdsr  23667  ngpds2  23668  ngpds2r  23669  ngpds3  23670  ngpds3r  23671  nmge0  23679  nmeq0  23680  nm2dif  23687  nmmul  23734  nlmmul0or  23753  nmods  23814  clmsub  24149  clmacl  24153  clmmcl  24154  clmsubcl  24155  clmvscl  24157  clmvsubval  24178  ncvsprp  24221  ncvsdif  24224  ncvspds  24230  cphnmvs  24259  cphipcl  24260  cphipcj  24268  cphorthcom  24270  cphipval2  24310  4cphipval2  24311  cphipval  24312  fmcfil  24341  mbfi1fseqlem3  24787  mbfi1fseqlem4  24788  mbfi1fseqlem5  24789  deg1ldgdomn  25164  drnguc1p  25240  quotval  25357  sincosq1sgn  25560  sincosq2sgn  25561  sincosq3sgn  25562  sincosq4sgn  25563  efabl  25611  lgsneg1  26375  dchrisumlem3  26544  ax5seglem2  27200  usgredg2vtx  27489  uspgredg2vtxeu  27490  usgredg2vtxeu  27491  cplgr3v  27705  vtxdumgr0nedg  27763  clwlkclwwlk  28267  frgrncvvdeqlem8  28571  grpocl  28763  grpodivcl  28802  ablomuldiv  28815  ablodivdiv4  28817  ablonnncan1  28820  vccl  28826  nvgcl  28883  nvcom  28884  nvadd4  28888  nvscl  28889  nvmval  28905  nvmcl  28909  nmcvcn  28958  nmlnoubi  29059  isblo3i  29064  blometi  29066  dipsubdir  29111  hlpar2  29159  hlpar  29160  hlcom  29163  hlipcj  29174  hlipgt0  29177  his52  29350  shintcli  29592  chlub  29772  homulass  30065  adjadj  30199  nmophmi  30294  kbass6  30384  atcvatlem  30648  mdsymlem3  30668  mdsymlem5  30670  suppiniseg  30922  rexdiv  31102  tlt3  31150  toslublem  31152  tosglblem  31154  archiabllem1b  31348  archiabllem2  31353  slmdacl  31364  slmdmcl  31365  slmdvacl  31367  qusscaval  31454  lidlincl  31509  cringm4  31524  aean  32112  fiunelcarsg  32183  probcun  32285  probdif  32287  cndprobin  32301  f1resrcmplf1dlem  32958  cusgredgex  32983  swrdwlk  32988  satefvfmla1  33287  climuzcnv  33529  pibt2  35515  matunitlindflem1  35700  mblfinlem1  35741  mblfinlem2  35742  ftc1anclem6  35782  ssbnd  35873  heibor1  35895  exidcl  35961  rngocl  35986  rngogcl  35997  rngocom  35998  rngoa4  36001  rngosub  36015  rngonegmn1l  36026  rngonegmn1r  36027  ispridlc  36155  lshpcmp  36929  opltcon3b  37145  oldmm1  37158  olj01  37166  latm32  37172  omllaw4  37187  omllaw5N  37188  cmtcomlemN  37189  cmt2N  37191  cmtbr2N  37194  cmtbr3N  37195  cmtbr4N  37196  glbconxN  37319  hlexch1  37323  hlexch2  37324  hlexchb1  37325  hlexchb2  37326  hlexch3  37332  hlexch4N  37333  hlatexchb1  37334  hlatexchb2  37335  hlatexch1  37336  hlatexch2  37337  hlatle  37339  hlateq  37340  hlrelat1  37341  hlrelat2  37344  cvr1  37351  cvrval5  37356  cvrp  37357  atcvr1  37358  atcvr2  37359  cvrexchlem  37360  cvrexch  37361  dalem54  37667  pmaple  37702  pmap11  37703  paddass  37779  pmapj2N  37870  pmapocjN  37871  trlval2  38104  nnproddivdvdsd  39937  isdomn4  40100  pwspjmhmmgpd  40192  fsuppssind  40205  mhphf  40208  0prjspnlem  40381  grumnudlem  41792  eelT00  42214  eelTTT  42215  eelT11  42216  eelT12  42218  eelTT1  42219  eelT01  42220  mullimc  43047  mullimcf  43054  stoweidlem52  43483  stoweidlem60  43491  focofob  44459  f1ocof1ob  44460  rngcl  45329  nzerooringczr  45518  ply1mulgsum  45619  itschlc0xyqsol1  46000  sinhpcosh  46328  reseccl  46341  recsccl  46342  recotcl  46343  onetansqsecsq  46349