Theorem syl3an1 1165

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

Syntax hints:   → wi 4   ∧ w3a 1089

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 210  df-an 400  df-3an 1091

This theorem is referenced by:  3adant1l  1178  3adant1r  1179  syl3an1b  1405  syl3an1br  1408  wefrc  5530  tz7.5  6212  f1ofvswap  7094  f1ofveu  7186  fovrnda  7357  suppvalfng  7888  smoiso  8077  odi  8285  nndi  8329  nnmsucr  8331  f1oen2g  8623  f1dom2g  8624  domssex2  8784  enfii  8841  ordunifi  8899  ackbij1lem16  9814  divneg  11489  divdiv32  11505  divneg2  11521  ltdiv2  11683  fimaxre  11741  fiminre  11744  suprzcl  12222  peano2uz  12462  infssuzle  12492  lbzbi  12497  zbtwnre  12507  irrmul  12535  supxrunb1  12874  expnlbnd  13765  hash1to3  14022  fun2dmnop  14026  brfi1uzind  14029  brcnvtrclfvcnv  14533  retancl  15666  tanneg  15672  demoivreALT  15725  dvdscmulr  15809  dvdsmulcr  15810  mulmoddvds  15854  gcd0id  16041  euclemma  16233  phiprmpw  16292  fermltl  16300  vdwapun  16490  vdwapid1  16491  cshwshashlem1  16612  fsets  16698  pospo  17805  tltnle  17882  latasymb  17902  mndcl  18135  imasmnd2  18164  gsumsgrpccat  18220  grpcl  18327  dfgrp2  18346  grprcan  18355  grpsubcl  18397  imasgrp2  18432  mhmid  18438  mhmmnd  18439  mulginvcom  18470  mulgnndir  18474  mulgnnass  18480  qusgrp  18553  ghmmulg  18588  ghmrn  18589  ghmeqker  18603  gsumccatsymgsn  18772  ablcom  19142  ablinvadd  19149  mulgmhm  19167  mulgghm  19168  ghmcmn  19171  odadd1  19187  odadd2  19188  srgcl  19481  srgacl  19493  srgcom  19494  ringcl  19533  crngcom  19534  ringacl  19550  imasring  19591  irredlmul  19680  rhmmul  19701  drngmcl  19734  isdrngd  19746  subrgacl  19765  subrgugrp  19773  srngadd  19847  srngmul  19848  idsrngd  19852  lmodacl  19864  lmodmcl  19865  lmodvacl  19867  lmodvsubcl  19898  lmod4  19903  lmodvaddsub4  19905  lmodvpncan  19906  lmodvnpcan  19907  lmodsubeq0  19912  pwssplit3  20052  islbs2  20145  islbs3  20146  lbsext  20154  rspssp  20218  zlmlmod  20443  psgnco  20499  ipdir  20555  ip2eq  20569  ocvin  20590  frlmsplit2  20689  ascldimul  20801  ascldimulOLD  20802  rnasclmulcl  20808  mplbas2  20953  coe1add  21139  coe1subfv  21141  coe1mul2  21144  ringvcl  21251  cramer  21542  chpmat1d  21687  filin  22705  filfinnfr  22728  filuni  22736  ufprim  22760  uffinfix  22778  hausflf  22848  uffcfflf  22890  cnextcn  22918  tmdmulg  22943  tsmsxplem1  23004  psmetcl  23159  xmetcl  23183  metcl  23184  meteq0  23191  metge0  23197  metsym  23202  metgt0  23211  blelrnps  23268  blelrn  23269  blssm  23270  blres  23283  mscl  23313  xmscl  23314  xmsge0  23315  xmseq0  23316  xmssym  23317  mopnin  23349  nmf2  23445  ngpdsr  23457  ngpds2  23458  ngpds2r  23459  ngpds3  23460  ngpds3r  23461  nmge0  23469  nmeq0  23470  nm2dif  23477  nmmul  23516  nlmmul0or  23535  nmods  23596  clmsub  23931  clmacl  23935  clmmcl  23936  clmsubcl  23937  clmvscl  23939  clmvsubval  23960  ncvsprp  24003  ncvsdif  24006  ncvspds  24012  cphnmvs  24041  cphipcl  24042  cphipcj  24050  cphorthcom  24052  cphipval2  24092  4cphipval2  24093  cphipval  24094  fmcfil  24123  mbfi1fseqlem3  24569  mbfi1fseqlem4  24570  mbfi1fseqlem5  24571  deg1ldgdomn  24946  drnguc1p  25022  quotval  25139  sincosq1sgn  25342  sincosq2sgn  25343  sincosq3sgn  25344  sincosq4sgn  25345  efabl  25393  lgsneg1  26157  dchrisumlem3  26326  ax5seglem2  26974  usgredg2vtx  27261  uspgredg2vtxeu  27262  usgredg2vtxeu  27263  cplgr3v  27477  vtxdumgr0nedg  27535  clwlkclwwlk  28039  frgrncvvdeqlem8  28343  grpocl  28535  grpodivcl  28574  ablomuldiv  28587  ablodivdiv4  28589  ablonnncan1  28592  vccl  28598  nvgcl  28655  nvcom  28656  nvadd4  28660  nvscl  28661  nvmval  28677  nvmcl  28681  nmcvcn  28730  nmlnoubi  28831  isblo3i  28836  blometi  28838  dipsubdir  28883  hlpar2  28931  hlpar  28932  hlcom  28935  hlipcj  28946  hlipgt0  28949  his52  29122  shintcli  29364  chlub  29544  homulass  29837  adjadj  29971  nmophmi  30066  kbass6  30156  atcvatlem  30420  mdsymlem3  30440  mdsymlem5  30442  suppiniseg  30694  rexdiv  30874  tlt3  30921  toslublem  30923  tosglblem  30925  archiabllem1b  31119  archiabllem2  31124  slmdacl  31135  slmdmcl  31136  slmdvacl  31138  qusscaval  31220  lidlincl  31275  cringm4  31290  aean  31878  fiunelcarsg  31949  probcun  32051  probdif  32053  cndprobin  32067  f1resrcmplf1dlem  32725  cusgredgex  32750  swrdwlk  32755  satefvfmla1  33054  climuzcnv  33296  pibt2  35274  matunitlindflem1  35459  mblfinlem1  35500  mblfinlem2  35501  ftc1anclem6  35541  ssbnd  35632  heibor1  35654  exidcl  35720  rngocl  35745  rngogcl  35756  rngocom  35757  rngoa4  35760  rngosub  35774  rngonegmn1l  35785  rngonegmn1r  35786  ispridlc  35914  lshpcmp  36688  opltcon3b  36904  oldmm1  36917  olj01  36925  latm32  36931  omllaw4  36946  omllaw5N  36947  cmtcomlemN  36948  cmt2N  36950  cmtbr2N  36953  cmtbr3N  36954  cmtbr4N  36955  glbconxN  37078  hlexch1  37082  hlexch2  37083  hlexchb1  37084  hlexchb2  37085  hlexch3  37091  hlexch4N  37092  hlatexchb1  37093  hlatexchb2  37094  hlatexch1  37095  hlatexch2  37096  hlatle  37098  hlateq  37099  hlrelat1  37100  hlrelat2  37103  cvr1  37110  cvrval5  37115  cvrp  37116  atcvr1  37117  atcvr2  37118  cvrexchlem  37119  cvrexch  37120  dalem54  37426  pmaple  37461  pmap11  37462  paddass  37538  pmapj2N  37629  pmapocjN  37630  trlval2  37863  nnproddivdvdsd  39692  isdomn4  39835  pwspjmhmmgpd  39920  fsuppssind  39933  mhphf  39936  0prjspnlem  40109  grumnudlem  41517  eelT00  41939  eelTTT  41940  eelT11  41941  eelT12  41943  eelTT1  41944  eelT01  41945  mullimc  42775  mullimcf  42782  stoweidlem52  43211  stoweidlem60  43219  focofob  44187  f1ocof1ob  44188  rngcl  45057  nzerooringczr  45246  ply1mulgsum  45347  itschlc0xyqsol1  45728  sinhpcosh  46056  reseccl  46069  recsccl  46070  recotcl  46071  onetansqsecsq  46077