Theorem syl3an1 1163

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 1152	. 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 207  df-an 396  df-3an 1088

This theorem is referenced by:  3adant1l  1177  3adant1r  1178  syl3an1b  1405  syl3an1br  1408  wefrc  5632  tz7.5  6353  f1cdmsn  7257  f1ofvswap  7281  f1ofveu  7381  fovcdmda  7560  suppvalfng  8146  smoiso  8331  odi  8543  nndi  8587  nnmsucr  8589  f1oen2g  8940  f1dom2g  8941  domssex2  9101  dif1ennn  9125  enfii  9150  phplem2  9169  php  9171  php3  9173  findcard3  9229  ordunifi  9237  nnsdomg  9246  ackbij1lem16  10187  divneg  11874  divdiv32  11890  divneg2  11906  ltdiv2  12069  fimaxre  12127  fiminre  12130  suprzcl  12614  peano2uz  12860  infssuzle  12890  lbzbi  12895  zbtwnre  12905  irrmul  12933  supxrunb1  13279  expnlbnd  14198  hash1to3  14457  fun2dmnop  14470  brfi1uzind  14473  brcnvtrclfvcnv  14971  retancl  16110  tanneg  16116  demoivreALT  16169  dvdscmulr  16254  dvdsmulcr  16255  mulmoddvds  16300  gcd0id  16489  euclemma  16683  phiprmpw  16746  fermltl  16754  vdwapun  16945  vdwapid1  16946  cshwshashlem1  17066  fsets  17139  pospo  18304  tltnle  18381  latasymb  18401  sgrpcl  18653  mndcl  18669  imasmnd2  18701  gsumsgrpccat  18767  grpcl  18873  dfgrp2  18894  grprcan  18905  grpsubcl  18952  imasgrp2  18987  mhmid  18995  mhmmnd  18996  mulginvcom  19031  mulgnndir  19035  mulgnnass  19041  qusgrp  19118  ghmmulg  19160  ghmrn  19161  ghmeqker  19175  gsumccatsymgsn  19356  ablcom  19729  ablinvadd  19737  mulgmhm  19757  mulgghm  19758  ghmcmn  19761  odadd1  19778  odadd2  19779  rngacl  20071  rngcl  20073  rngpropd  20083  srgcl  20102  srgacl  20114  srgcom  20115  ringcl  20159  crngcom  20160  ringacl  20187  pwspjmhmmgpd  20237  imasring  20239  irredlmul  20337  rhmmul  20395  subrngacl  20465  subrgacl  20492  subrgmcl  20493  subrgugrp  20500  isdomn4  20625  drngmclOLD  20660  isdrngd  20674  isdrngdOLD  20676  srngadd  20760  srngmul  20761  idsrngd  20765  lmodacl  20778  lmodmcl  20779  lmodvacl  20781  lmodvsubcl  20813  lmod4  20818  lmodvaddsub4  20820  lmodvpncan  20821  lmodvnpcan  20822  lmodsubeq0  20827  pwssplit3  20968  islbs2  21064  islbs3  21065  lbsext  21073  rspssp  21149  nzerooringczr  21390  zlmlmod  21432  psgnco  21492  ipdir  21548  ip2eq  21562  ocvin  21583  frlmsplit2  21682  ascldimul  21797  rnasclmulcl  21803  mplbas2  21949  coe1add  22150  coe1subfv  22152  coe1mul2  22155  rhmply1vsca  22275  ringvcl  22287  cramer  22578  chpmat1d  22723  filin  23741  filfinnfr  23764  filuni  23772  ufprim  23796  uffinfix  23814  hausflf  23884  uffcfflf  23926  cnextcn  23954  tmdmulg  23979  tsmsxplem1  24040  psmetcl  24195  xmetcl  24219  metcl  24220  meteq0  24227  metge0  24233  metsym  24238  metgt0  24247  blelrnps  24304  blelrn  24305  blssm  24306  blres  24319  mscl  24349  xmscl  24350  xmsge0  24351  xmseq0  24352  xmssym  24353  mopnin  24385  nmf2  24481  ngpdsr  24493  ngpds2  24494  ngpds2r  24495  ngpds3  24496  ngpds3r  24497  nmge0  24505  nmeq0  24506  nm2dif  24513  nmmul  24552  nlmmul0or  24571  nmods  24632  clmsub  24980  clmacl  24984  clmmcl  24985  clmsubcl  24986  clmvscl  24988  clmvsubval  25009  ncvsprp  25052  ncvsdif  25055  ncvspds  25061  cphnmvs  25090  cphipcl  25091  cphipcj  25099  cphorthcom  25101  cphipval2  25141  4cphipval2  25142  cphipval  25143  fmcfil  25172  mbfi1fseqlem3  25618  mbfi1fseqlem4  25619  mbfi1fseqlem5  25620  deg1ldgdomn  25999  drnguc1p  26079  quotval  26200  sincosq1sgn  26407  sincosq2sgn  26408  sincosq3sgn  26409  sincosq4sgn  26410  efabl  26459  lgsneg1  27233  dchrisumlem3  27402  bdayn0p1  28258  ax5seglem2  28856  usgredg2vtx  29146  uspgredg2vtxeu  29147  usgredg2vtxeu  29148  cplgr3v  29362  vtxdumgr0nedg  29421  clwlkclwwlk  29931  frgrncvvdeqlem8  30235  grpocl  30429  grpodivcl  30468  ablomuldiv  30481  ablodivdiv4  30483  ablonnncan1  30486  vccl  30492  nvgcl  30549  nvcom  30550  nvadd4  30554  nvscl  30555  nvmval  30571  nvmcl  30575  nmcvcn  30624  nmlnoubi  30725  isblo3i  30730  blometi  30732  dipsubdir  30777  hlpar2  30825  hlpar  30826  hlcom  30829  hlipcj  30840  hlipgt0  30843  his52  31016  shintcli  31258  chlub  31438  homulass  31731  adjadj  31865  nmophmi  31960  kbass6  32050  atcvatlem  32314  mdsymlem3  32334  mdsymlem5  32336  suppiniseg  32609  rexdiv  32846  tlt3  32896  toslublem  32898  tosglblem  32900  archiabllem1b  33146  archiabllem2  33151  slmdacl  33162  slmdmcl  33163  slmdvacl  33165  lidlincl  33401  cringm4  33417  evls1fldgencl  33665  aean  34234  fiunelcarsg  34307  probcun  34409  probdif  34411  cndprobin  34425  f1resrcmplf1dlem  35076  cusgredgex  35109  swrdwlk  35114  satefvfmla1  35412  climuzcnv  35658  pibt2  37405  matunitlindflem1  37610  mblfinlem1  37651  mblfinlem2  37652  ftc1anclem6  37692  ssbnd  37782  heibor1  37804  exidcl  37870  rngocl  37895  rngogcl  37906  rngocom  37907  rngoa4  37910  rngosub  37924  rngonegmn1l  37935  rngonegmn1r  37936  ispridlc  38064  lshpcmp  38981  opltcon3b  39197  oldmm1  39210  olj01  39218  latm32  39224  omllaw4  39239  omllaw5N  39240  cmtcomlemN  39241  cmt2N  39243  cmtbr2N  39246  cmtbr3N  39247  cmtbr4N  39248  glbconxN  39372  hlexch1  39376  hlexch2  39377  hlexchb1  39378  hlexchb2  39379  hlexch3  39385  hlexch4N  39386  hlatexchb1  39387  hlatexchb2  39388  hlatexch1  39389  hlatexch2  39390  hlatle  39392  hlateq  39393  hlrelat1  39394  hlrelat2  39397  cvr1  39404  cvrval5  39409  cvrp  39410  atcvr1  39411  atcvr2  39412  cvrexchlem  39413  cvrexch  39414  dalem54  39720  pmaple  39755  pmap11  39756  paddass  39832  pmapj2N  39923  pmapocjN  39924  trlval2  40157  nnproddivdvdsd  41988  fsuppssind  42581  mhphf  42585  0prjspnlem  42611  grumnudlem  44274  eelT00  44694  eelTTT  44695  eelT11  44696  eelT12  44698  eelTT1  44699  eelT01  44700  mullimc  45614  mullimcf  45621  dvmptfprod  45943  stoweidlem52  46050  stoweidlem60  46058  focofob  47081  f1ocof1ob  47082  clnbgrgrim  47934  ply1mulgsum  48379  itschlc0xyqsol1  48755  sinhpcosh  49729  reseccl  49742  recsccl  49743  recotcl  49744  onetansqsecsq  49750