Theorem syl3an1 1162

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

Syntax hints:   → wi 4   ∧ w3a 1086

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 397  df-3an 1088

This theorem is referenced by:  3adant1l  1175  3adant1r  1176  syl3an1b  1402  syl3an1br  1405  wefrc  5584  tz7.5  6291  f1cdmsn  7163  f1ofvswap  7187  f1ofveu  7279  fovrnda  7452  suppvalfng  7993  smoiso  8202  odi  8419  nndi  8463  nnmsucr  8465  f1oen2g  8765  f1dom2g  8766  f1dom2gOLD  8767  domssex2  8933  enfii  8981  phplem2  9000  php  9002  php3  9004  sucdom  9027  ordunifi  9073  ackbij1lem16  10000  divneg  11676  divdiv32  11692  divneg2  11708  ltdiv2  11870  fimaxre  11928  fiminre  11931  suprzcl  12409  peano2uz  12650  infssuzle  12680  lbzbi  12685  zbtwnre  12695  irrmul  12723  supxrunb1  13062  expnlbnd  13957  hash1to3  14214  fun2dmnop  14218  brfi1uzind  14221  brcnvtrclfvcnv  14725  retancl  15860  tanneg  15866  demoivreALT  15919  dvdscmulr  16003  dvdsmulcr  16004  mulmoddvds  16048  gcd0id  16235  euclemma  16427  phiprmpw  16486  fermltl  16494  vdwapun  16684  vdwapid1  16685  cshwshashlem1  16806  fsets  16879  pospo  18072  tltnle  18149  latasymb  18169  mndcl  18402  imasmnd2  18431  gsumsgrpccat  18487  grpcl  18594  dfgrp2  18613  grprcan  18622  grpsubcl  18664  imasgrp2  18699  mhmid  18705  mhmmnd  18706  mulginvcom  18737  mulgnndir  18741  mulgnnass  18747  qusgrp  18820  ghmmulg  18855  ghmrn  18856  ghmeqker  18870  gsumccatsymgsn  19043  ablcom  19413  ablinvadd  19420  mulgmhm  19438  mulgghm  19439  ghmcmn  19442  odadd1  19458  odadd2  19459  srgcl  19757  srgacl  19769  srgcom  19770  ringcl  19809  crngcom  19810  ringacl  19826  imasring  19867  irredlmul  19959  rhmmul  19980  drngmcl  20013  isdrngd  20025  subrgacl  20044  subrgugrp  20052  srngadd  20126  srngmul  20127  idsrngd  20131  lmodacl  20143  lmodmcl  20144  lmodvacl  20146  lmodvsubcl  20177  lmod4  20182  lmodvaddsub4  20184  lmodvpncan  20185  lmodvnpcan  20186  lmodsubeq0  20191  pwssplit3  20332  islbs2  20425  islbs3  20426  lbsext  20434  rspssp  20506  zlmlmod  20737  psgnco  20797  ipdir  20853  ip2eq  20867  ocvin  20888  frlmsplit2  20989  ascldimul  21101  rnasclmulcl  21107  mplbas2  21252  coe1add  21444  coe1subfv  21446  coe1mul2  21449  ringvcl  21556  cramer  21849  chpmat1d  21994  filin  23014  filfinnfr  23037  filuni  23045  ufprim  23069  uffinfix  23087  hausflf  23157  uffcfflf  23199  cnextcn  23227  tmdmulg  23252  tsmsxplem1  23313  psmetcl  23469  xmetcl  23493  metcl  23494  meteq0  23501  metge0  23507  metsym  23512  metgt0  23521  blelrnps  23578  blelrn  23579  blssm  23580  blres  23593  mscl  23623  xmscl  23624  xmsge0  23625  xmseq0  23626  xmssym  23627  mopnin  23662  nmf2  23758  ngpdsr  23770  ngpds2  23771  ngpds2r  23772  ngpds3  23773  ngpds3r  23774  nmge0  23782  nmeq0  23783  nm2dif  23790  nmmul  23837  nlmmul0or  23856  nmods  23917  clmsub  24252  clmacl  24256  clmmcl  24257  clmsubcl  24258  clmvscl  24260  clmvsubval  24281  ncvsprp  24325  ncvsdif  24328  ncvspds  24334  cphnmvs  24363  cphipcl  24364  cphipcj  24372  cphorthcom  24374  cphipval2  24414  4cphipval2  24415  cphipval  24416  fmcfil  24445  mbfi1fseqlem3  24891  mbfi1fseqlem4  24892  mbfi1fseqlem5  24893  deg1ldgdomn  25268  drnguc1p  25344  quotval  25461  sincosq1sgn  25664  sincosq2sgn  25665  sincosq3sgn  25666  sincosq4sgn  25667  efabl  25715  lgsneg1  26479  dchrisumlem3  26648  ax5seglem2  27306  usgredg2vtx  27595  uspgredg2vtxeu  27596  usgredg2vtxeu  27597  cplgr3v  27811  vtxdumgr0nedg  27869  clwlkclwwlk  28375  frgrncvvdeqlem8  28679  grpocl  28871  grpodivcl  28910  ablomuldiv  28923  ablodivdiv4  28925  ablonnncan1  28928  vccl  28934  nvgcl  28991  nvcom  28992  nvadd4  28996  nvscl  28997  nvmval  29013  nvmcl  29017  nmcvcn  29066  nmlnoubi  29167  isblo3i  29172  blometi  29174  dipsubdir  29219  hlpar2  29267  hlpar  29268  hlcom  29271  hlipcj  29282  hlipgt0  29285  his52  29458  shintcli  29700  chlub  29880  homulass  30173  adjadj  30307  nmophmi  30402  kbass6  30492  atcvatlem  30756  mdsymlem3  30776  mdsymlem5  30778  suppiniseg  31029  rexdiv  31209  tlt3  31257  toslublem  31259  tosglblem  31261  archiabllem1b  31455  archiabllem2  31460  slmdacl  31471  slmdmcl  31472  slmdvacl  31474  qusscaval  31561  lidlincl  31616  cringm4  31631  aean  32221  fiunelcarsg  32292  probcun  32394  probdif  32396  cndprobin  32410  f1resrcmplf1dlem  33067  cusgredgex  33092  swrdwlk  33097  satefvfmla1  33396  climuzcnv  33638  pibt2  35597  matunitlindflem1  35782  mblfinlem1  35823  mblfinlem2  35824  ftc1anclem6  35864  ssbnd  35955  heibor1  35977  exidcl  36043  rngocl  36068  rngogcl  36079  rngocom  36080  rngoa4  36083  rngosub  36097  rngonegmn1l  36108  rngonegmn1r  36109  ispridlc  36237  lshpcmp  37009  opltcon3b  37225  oldmm1  37238  olj01  37246  latm32  37252  omllaw4  37267  omllaw5N  37268  cmtcomlemN  37269  cmt2N  37271  cmtbr2N  37274  cmtbr3N  37275  cmtbr4N  37276  glbconxN  37399  hlexch1  37403  hlexch2  37404  hlexchb1  37405  hlexchb2  37406  hlexch3  37412  hlexch4N  37413  hlatexchb1  37414  hlatexchb2  37415  hlatexch1  37416  hlatexch2  37417  hlatle  37419  hlateq  37420  hlrelat1  37421  hlrelat2  37424  cvr1  37431  cvrval5  37436  cvrp  37437  atcvr1  37438  atcvr2  37439  cvrexchlem  37440  cvrexch  37441  dalem54  37747  pmaple  37782  pmap11  37783  paddass  37859  pmapj2N  37950  pmapocjN  37951  trlval2  38184  nnproddivdvdsd  40016  isdomn4  40179  pwspjmhmmgpd  40274  fsuppssind  40289  mhphf  40292  0prjspnlem  40467  grumnudlem  41910  eelT00  42332  eelTTT  42333  eelT11  42334  eelT12  42336  eelTT1  42337  eelT01  42338  mullimc  43164  mullimcf  43171  stoweidlem52  43600  stoweidlem60  43608  focofob  44583  f1ocof1ob  44584  rngcl  45452  nzerooringczr  45641  ply1mulgsum  45742  itschlc0xyqsol1  46123  sinhpcosh  46453  reseccl  46466  recsccl  46467  recotcl  46468  onetansqsecsq  46474