Theorem syl3an1 1169

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

Syntax hints:   → wi 4   ∧ w3a 1092

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

This theorem is referenced by:  3adant1l  1183  3adant1r  1184  syl3an1b  1411  syl3an1br  1414  wefrc  5612  tz7.5  6331  f1cdmsn  7226  f1ofvswap  7250  f1ofveu  7350  fovcdmda  7527  suppvalfng  8107  smoiso  8292  odi  8504  nndi  8549  nnmsucr  8551  f1oen2g  8905  f1dom2g  8906  domssex2  9065  dif1ennn  9087  enfii  9110  phplem2  9129  php  9131  php3  9133  findcard3  9183  ordunifi  9190  nnsdomg  9199  ackbij1lem16  10147  divneg  11837  divdiv32  11854  divneg2  11870  ltdiv2  12033  fimaxre  12091  fiminre  12094  suprzcl  12600  peano2uz  12842  infssuzle  12872  lbzbi  12877  zbtwnre  12887  irrmul  12915  supxrunb1  13262  expnlbnd  14186  hash1to3  14445  fun2dmnop  14458  brfi1uzind  14461  brcnvtrclfvcnv  14958  retancl  16100  tanneg  16106  demoivreALT  16159  dvdscmulr  16244  dvdsmulcr  16245  mulmoddvds  16290  gcd0id  16479  euclemma  16674  phiprmpw  16737  fermltl  16745  vdwapun  16936  vdwapid1  16937  cshwshashlem1  17057  fsets  17130  pospo  18300  tltnle  18377  latasymb  18399  sgrpcl  18685  mndcl  18701  imasmnd2  18733  gsumsgrpccat  18799  grpcl  18908  dfgrp2  18929  grprcan  18940  grpsubcl  18987  imasgrp2  19022  mhmid  19030  mhmmnd  19031  mulginvcom  19066  mulgnndir  19070  mulgnnass  19076  qusgrp  19152  ghmmulg  19194  ghmrn  19195  ghmeqker  19209  gsumccatsymgsn  19392  ablcom  19765  ablinvadd  19773  mulgmhm  19793  mulgghm  19794  ghmcmn  19797  odadd1  19814  odadd2  19815  rngacl  20134  rngcl  20136  rngpropd  20146  srgcl  20165  srgacl  20177  srgcom  20178  ringcl  20222  crngcom  20223  ringacl  20250  pwspjmhmmgpd  20298  imasring  20301  irredlmul  20399  rhmmul  20457  subrngacl  20528  subrgacl  20555  subrgmcl  20556  subrgugrp  20563  isdomn4  20688  drngmclOLD  20723  isdrngd  20737  isdrngdOLD  20739  srngadd  20823  srngmul  20824  idsrngd  20828  lmodacl  20862  lmodmcl  20863  lmodvacl  20865  lmodvsubcl  20897  lmod4  20902  lmodvaddsub4  20904  lmodvpncan  20905  lmodvnpcan  20906  lmodsubeq0  20911  pwssplit3  21051  islbs2  21147  islbs3  21148  lbsext  21156  rspssp  21232  nzerooringczr  21455  zlmlmod  21497  psgnco  21558  ipdir  21614  ip2eq  21628  ocvin  21649  frlmsplit2  21748  ascldimul  21863  rnasclmulcl  21869  mplbas2  22018  coe1add  22250  coe1subfv  22252  coe1mul2  22255  rhmply1vsca  22371  ringvcl  22383  cramer  22674  chpmat1d  22819  filin  23837  filfinnfr  23860  filuni  23868  ufprim  23892  uffinfix  23910  hausflf  23980  uffcfflf  24022  cnextcn  24050  tmdmulg  24075  tsmsxplem1  24136  psmetcl  24290  xmetcl  24314  metcl  24315  meteq0  24322  metge0  24328  metsym  24333  metgt0  24342  blelrnps  24399  blelrn  24400  blssm  24401  blres  24414  mscl  24444  xmscl  24445  xmsge0  24446  xmseq0  24447  xmssym  24448  mopnin  24480  nmf2  24576  ngpdsr  24588  ngpds2  24589  ngpds2r  24590  ngpds3  24591  ngpds3r  24592  nmge0  24600  nmeq0  24601  nm2dif  24608  nmmul  24647  nlmmul0or  24666  nmods  24727  clmsub  25065  clmacl  25069  clmmcl  25070  clmsubcl  25071  clmvscl  25073  clmvsubval  25094  ncvsprp  25137  ncvsdif  25140  ncvspds  25146  cphnmvs  25175  cphipcl  25176  cphipcj  25184  cphorthcom  25186  cphipval2  25226  4cphipval2  25227  cphipval  25228  fmcfil  25257  mbfi1fseqlem3  25702  mbfi1fseqlem4  25703  mbfi1fseqlem5  25704  deg1ldgdomn  26077  drnguc1p  26157  quotval  26276  sincosq1sgn  26480  sincosq2sgn  26481  sincosq3sgn  26482  sincosq4sgn  26483  efabl  26532  lgsneg1  27303  dchrisumlem3  27472  bdayn0p1  28379  ax5seglem2  29016  usgredg2vtx  29306  uspgredg2vtxeu  29307  usgredg2vtxeu  29308  cplgr3v  29522  vtxdumgr0nedg  29580  clwlkclwwlk  30090  frgrncvvdeqlem8  30394  grpocl  30589  grpodivcl  30628  ablomuldiv  30641  ablodivdiv4  30643  ablonnncan1  30646  vccl  30652  nvgcl  30709  nvcom  30710  nvadd4  30714  nvscl  30715  nvmval  30731  nvmcl  30735  nmcvcn  30784  nmlnoubi  30885  isblo3i  30890  blometi  30892  dipsubdir  30937  hlpar2  30985  hlpar  30986  hlcom  30989  hlipcj  31000  hlipgt0  31003  his52  31176  shintcli  31418  chlub  31598  homulass  31891  adjadj  32025  nmophmi  32120  kbass6  32210  atcvatlem  32474  mdsymlem3  32494  mdsymlem5  32496  suppiniseg  32778  rexdiv  33004  tlt3  33049  toslublem  33051  tosglblem  33053  archiabllem1b  33273  archiabllem2  33278  slmdacl  33290  slmdmcl  33291  slmdvacl  33293  lidlincl  33513  cringm4  33529  evls1fldgencl  33854  aean  34428  fiunelcarsg  34500  probcun  34602  probdif  34604  cndprobin  34618  f1resrcmplf1dlem  35267  rankfilimbi  35282  cusgredgex  35350  swrdwlk  35355  satefvfmla1  35653  climuzcnv  35899  pibt2  37779  matunitlindflem1  37983  mblfinlem1  38024  mblfinlem2  38025  ftc1anclem6  38065  ssbnd  38155  heibor1  38177  exidcl  38243  rngocl  38268  rngogcl  38279  rngocom  38280  rngoa4  38283  rngosub  38297  rngonegmn1l  38308  rngonegmn1r  38309  ispridlc  38437  lshpcmp  39480  opltcon3b  39696  oldmm1  39709  olj01  39717  latm32  39723  omllaw4  39738  omllaw5N  39739  cmtcomlemN  39740  cmt2N  39742  cmtbr2N  39745  cmtbr3N  39746  cmtbr4N  39747  glbconxN  39870  hlexch1  39874  hlexch2  39875  hlexchb1  39876  hlexchb2  39877  hlexch3  39883  hlexch4N  39884  hlatexchb1  39885  hlatexchb2  39886  hlatexch1  39887  hlatexch2  39888  hlatle  39890  hlateq  39891  hlrelat1  39892  hlrelat2  39895  cvr1  39902  cvrval5  39907  cvrp  39908  atcvr1  39909  atcvr2  39910  cvrexchlem  39911  cvrexch  39912  dalem54  40218  pmaple  40253  pmap11  40254  paddass  40330  pmapj2N  40421  pmapocjN  40422  trlval2  40655  nnproddivdvdsd  42485  fsuppssind  43043  mhphf  43047  0prjspnlem  43073  grumnudlem  44729  eelT00  45148  eelTTT  45149  eelT11  45150  eelT12  45152  eelTT1  45153  eelT01  45154  mullimc  46061  mullimcf  46068  dvmptfprod  46388  stoweidlem52  46495  stoweidlem60  46503  focofob  47543  f1ocof1ob  47544  clnbgrgrim  48425  ply1mulgsum  48881  itschlc0xyqsol1  49257  sinhpcosh  50230  reseccl  50243  recsccl  50244  recotcl  50245  onetansqsecsq  50251