Theorem syl3an1 1164

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

Syntax hints:   → wi 4   ∧ w3a 1088

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 398  df-3an 1090

This theorem is referenced by:  3adant1l  1177  3adant1r  1178  syl3an1b  1404  syl3an1br  1407  wefrc  5671  tz7.5  6386  f1cdmsn  7280  f1ofvswap  7304  f1ofveu  7403  fovcdmda  7578  suppvalfng  8153  smoiso  8362  odi  8579  nndi  8623  nnmsucr  8625  f1oen2g  8964  f1dom2g  8965  f1dom2gOLD  8966  domssex2  9137  dif1ennn  9161  enfii  9189  phplem2  9208  php  9210  php3  9212  findcard3  9285  ordunifi  9293  nnsdomg  9302  ackbij1lem16  10230  divneg  11906  divdiv32  11922  divneg2  11938  ltdiv2  12100  fimaxre  12158  fiminre  12161  suprzcl  12642  peano2uz  12885  infssuzle  12915  lbzbi  12920  zbtwnre  12930  irrmul  12958  supxrunb1  13298  expnlbnd  14196  hash1to3  14452  fun2dmnop  14456  brfi1uzind  14459  brcnvtrclfvcnv  14952  retancl  16085  tanneg  16091  demoivreALT  16144  dvdscmulr  16228  dvdsmulcr  16229  mulmoddvds  16273  gcd0id  16460  euclemma  16650  phiprmpw  16709  fermltl  16717  vdwapun  16907  vdwapid1  16908  cshwshashlem1  17029  fsets  17102  pospo  18298  tltnle  18375  latasymb  18395  sgrpcl  18617  mndcl  18633  imasmnd2  18662  gsumsgrpccat  18721  grpcl  18827  dfgrp2  18847  grprcan  18858  grpsubcl  18903  imasgrp2  18938  mhmid  18946  mhmmnd  18947  mulginvcom  18979  mulgnndir  18983  mulgnnass  18989  qusgrp  19065  ghmmulg  19104  ghmrn  19105  ghmeqker  19119  gsumccatsymgsn  19294  ablcom  19667  ablinvadd  19675  mulgmhm  19695  mulgghm  19696  ghmcmn  19699  odadd1  19716  odadd2  19717  srgcl  20016  srgacl  20028  srgcom  20029  ringcl  20073  crngcom  20074  ringacl  20095  pwspjmhmmgpd  20141  imasring  20143  irredlmul  20242  rhmmul  20264  subrgacl  20330  subrgugrp  20338  drngmcl  20374  isdrngd  20390  isdrngdOLD  20392  srngadd  20465  srngmul  20466  idsrngd  20470  lmodacl  20483  lmodmcl  20484  lmodvacl  20486  lmodvsubcl  20517  lmod4  20522  lmodvaddsub4  20524  lmodvpncan  20525  lmodvnpcan  20526  lmodsubeq0  20531  pwssplit3  20672  islbs2  20767  islbs3  20768  lbsext  20776  rspssp  20851  isdomn4  20918  zlmlmod  21076  psgnco  21136  ipdir  21192  ip2eq  21206  ocvin  21227  frlmsplit2  21328  ascldimul  21442  rnasclmulcl  21448  mplbas2  21597  coe1add  21786  coe1subfv  21788  coe1mul2  21791  ringvcl  21900  cramer  22193  chpmat1d  22338  filin  23358  filfinnfr  23381  filuni  23389  ufprim  23413  uffinfix  23431  hausflf  23501  uffcfflf  23543  cnextcn  23571  tmdmulg  23596  tsmsxplem1  23657  psmetcl  23813  xmetcl  23837  metcl  23838  meteq0  23845  metge0  23851  metsym  23856  metgt0  23865  blelrnps  23922  blelrn  23923  blssm  23924  blres  23937  mscl  23967  xmscl  23968  xmsge0  23969  xmseq0  23970  xmssym  23971  mopnin  24006  nmf2  24102  ngpdsr  24114  ngpds2  24115  ngpds2r  24116  ngpds3  24117  ngpds3r  24118  nmge0  24126  nmeq0  24127  nm2dif  24134  nmmul  24181  nlmmul0or  24200  nmods  24261  clmsub  24596  clmacl  24600  clmmcl  24601  clmsubcl  24602  clmvscl  24604  clmvsubval  24625  ncvsprp  24669  ncvsdif  24672  ncvspds  24678  cphnmvs  24707  cphipcl  24708  cphipcj  24716  cphorthcom  24718  cphipval2  24758  4cphipval2  24759  cphipval  24760  fmcfil  24789  mbfi1fseqlem3  25235  mbfi1fseqlem4  25236  mbfi1fseqlem5  25237  deg1ldgdomn  25612  drnguc1p  25688  quotval  25805  sincosq1sgn  26008  sincosq2sgn  26009  sincosq3sgn  26010  sincosq4sgn  26011  efabl  26059  lgsneg1  26825  dchrisumlem3  26994  ax5seglem2  28218  usgredg2vtx  28507  uspgredg2vtxeu  28508  usgredg2vtxeu  28509  cplgr3v  28723  vtxdumgr0nedg  28781  clwlkclwwlk  29286  frgrncvvdeqlem8  29590  grpocl  29784  grpodivcl  29823  ablomuldiv  29836  ablodivdiv4  29838  ablonnncan1  29841  vccl  29847  nvgcl  29904  nvcom  29905  nvadd4  29909  nvscl  29910  nvmval  29926  nvmcl  29930  nmcvcn  29979  nmlnoubi  30080  isblo3i  30085  blometi  30087  dipsubdir  30132  hlpar2  30180  hlpar  30181  hlcom  30184  hlipcj  30195  hlipgt0  30198  his52  30371  shintcli  30613  chlub  30793  homulass  31086  adjadj  31220  nmophmi  31315  kbass6  31405  atcvatlem  31669  mdsymlem3  31689  mdsymlem5  31691  suppiniseg  31939  rexdiv  32123  tlt3  32171  toslublem  32173  tosglblem  32175  archiabllem1b  32369  archiabllem2  32374  slmdacl  32385  slmdmcl  32386  slmdvacl  32388  lidlincl  32579  cringm4  32596  aean  33273  fiunelcarsg  33346  probcun  33448  probdif  33450  cndprobin  33464  f1resrcmplf1dlem  34120  cusgredgex  34143  swrdwlk  34148  satefvfmla1  34447  climuzcnv  34687  pibt2  36346  matunitlindflem1  36532  mblfinlem1  36573  mblfinlem2  36574  ftc1anclem6  36614  ssbnd  36704  heibor1  36726  exidcl  36792  rngocl  36817  rngogcl  36828  rngocom  36829  rngoa4  36832  rngosub  36846  rngonegmn1l  36857  rngonegmn1r  36858  ispridlc  36986  lshpcmp  37906  opltcon3b  38122  oldmm1  38135  olj01  38143  latm32  38149  omllaw4  38164  omllaw5N  38165  cmtcomlemN  38166  cmt2N  38168  cmtbr2N  38171  cmtbr3N  38172  cmtbr4N  38173  glbconxN  38297  hlexch1  38301  hlexch2  38302  hlexchb1  38303  hlexchb2  38304  hlexch3  38310  hlexch4N  38311  hlatexchb1  38312  hlatexchb2  38313  hlatexch1  38314  hlatexch2  38315  hlatle  38317  hlateq  38318  hlrelat1  38319  hlrelat2  38322  cvr1  38329  cvrval5  38334  cvrp  38335  atcvr1  38336  atcvr2  38337  cvrexchlem  38338  cvrexch  38339  dalem54  38645  pmaple  38680  pmap11  38681  paddass  38757  pmapj2N  38848  pmapocjN  38849  trlval2  39082  nnproddivdvdsd  40914  fsuppssind  41213  mhphf  41217  0prjspnlem  41413  grumnudlem  43092  eelT00  43514  eelTTT  43515  eelT11  43516  eelT12  43518  eelTT1  43519  eelT01  43520  mullimc  44380  mullimcf  44387  stoweidlem52  44816  stoweidlem60  44824  focofob  45836  f1ocof1ob  45837  rngacl  46709  rngcl  46711  rngpropd  46721  subrngacl  46783  nzerooringczr  47018  ply1mulgsum  47119  itschlc0xyqsol1  47500  sinhpcosh  47833  reseccl  47846  recsccl  47847  recotcl  47848  onetansqsecsq  47854