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

This theorem is referenced by:  3adant1l  1175  3adant1r  1176  syl3an1b  1402  syl3an1br  1405  wefrc  5682  tz7.5  6406  f1cdmsn  7301  f1ofvswap  7325  f1ofveu  7424  fovcdmda  7603  suppvalfng  8190  smoiso  8400  odi  8615  nndi  8659  nnmsucr  8661  f1oen2g  9007  f1dom2g  9008  domssex2  9175  dif1ennn  9199  enfii  9223  phplem2  9242  php  9244  php3  9246  findcard3  9315  ordunifi  9323  nnsdomg  9332  ackbij1lem16  10271  divneg  11956  divdiv32  11972  divneg2  11988  ltdiv2  12151  fimaxre  12209  fiminre  12212  suprzcl  12695  peano2uz  12940  infssuzle  12970  lbzbi  12975  zbtwnre  12985  irrmul  13013  supxrunb1  13357  expnlbnd  14268  hash1to3  14527  fun2dmnop  14540  brfi1uzind  14543  brcnvtrclfvcnv  15040  retancl  16174  tanneg  16180  demoivreALT  16233  dvdscmulr  16318  dvdsmulcr  16319  mulmoddvds  16363  gcd0id  16552  euclemma  16746  phiprmpw  16809  fermltl  16817  vdwapun  17007  vdwapid1  17008  cshwshashlem1  17129  fsets  17202  pospo  18402  tltnle  18479  latasymb  18499  sgrpcl  18751  mndcl  18767  imasmnd2  18799  gsumsgrpccat  18865  grpcl  18971  dfgrp2  18992  grprcan  19003  grpsubcl  19050  imasgrp2  19085  mhmid  19093  mhmmnd  19094  mulginvcom  19129  mulgnndir  19133  mulgnnass  19139  qusgrp  19216  ghmmulg  19258  ghmrn  19259  ghmeqker  19273  gsumccatsymgsn  19458  ablcom  19831  ablinvadd  19839  mulgmhm  19859  mulgghm  19860  ghmcmn  19863  odadd1  19880  odadd2  19881  rngacl  20179  rngcl  20181  rngpropd  20191  srgcl  20210  srgacl  20222  srgcom  20223  ringcl  20267  crngcom  20268  ringacl  20291  pwspjmhmmgpd  20341  imasring  20343  irredlmul  20444  rhmmul  20502  subrngacl  20572  subrgacl  20599  subrgmcl  20600  subrgugrp  20607  isdomn4  20732  drngmclOLD  20767  isdrngd  20781  isdrngdOLD  20783  srngadd  20868  srngmul  20869  idsrngd  20873  lmodacl  20886  lmodmcl  20887  lmodvacl  20889  lmodvsubcl  20921  lmod4  20926  lmodvaddsub4  20928  lmodvpncan  20929  lmodvnpcan  20930  lmodsubeq0  20935  pwssplit3  21077  islbs2  21173  islbs3  21174  lbsext  21182  rspssp  21266  nzerooringczr  21508  zlmlmod  21554  psgnco  21618  ipdir  21674  ip2eq  21688  ocvin  21709  frlmsplit2  21810  ascldimul  21925  rnasclmulcl  21931  mplbas2  22077  coe1add  22282  coe1subfv  22284  coe1mul2  22287  rhmply1vsca  22407  ringvcl  22419  cramer  22712  chpmat1d  22857  filin  23877  filfinnfr  23900  filuni  23908  ufprim  23932  uffinfix  23950  hausflf  24020  uffcfflf  24062  cnextcn  24090  tmdmulg  24115  tsmsxplem1  24176  psmetcl  24332  xmetcl  24356  metcl  24357  meteq0  24364  metge0  24370  metsym  24375  metgt0  24384  blelrnps  24441  blelrn  24442  blssm  24443  blres  24456  mscl  24486  xmscl  24487  xmsge0  24488  xmseq0  24489  xmssym  24490  mopnin  24525  nmf2  24621  ngpdsr  24633  ngpds2  24634  ngpds2r  24635  ngpds3  24636  ngpds3r  24637  nmge0  24645  nmeq0  24646  nm2dif  24653  nmmul  24700  nlmmul0or  24719  nmods  24780  clmsub  25126  clmacl  25130  clmmcl  25131  clmsubcl  25132  clmvscl  25134  clmvsubval  25155  ncvsprp  25199  ncvsdif  25202  ncvspds  25208  cphnmvs  25237  cphipcl  25238  cphipcj  25246  cphorthcom  25248  cphipval2  25288  4cphipval2  25289  cphipval  25290  fmcfil  25319  mbfi1fseqlem3  25766  mbfi1fseqlem4  25767  mbfi1fseqlem5  25768  deg1ldgdomn  26147  drnguc1p  26227  quotval  26348  sincosq1sgn  26554  sincosq2sgn  26555  sincosq3sgn  26556  sincosq4sgn  26557  efabl  26606  lgsneg1  27380  dchrisumlem3  27549  ax5seglem2  28958  usgredg2vtx  29250  uspgredg2vtxeu  29251  usgredg2vtxeu  29252  cplgr3v  29466  vtxdumgr0nedg  29525  clwlkclwwlk  30030  frgrncvvdeqlem8  30334  grpocl  30528  grpodivcl  30567  ablomuldiv  30580  ablodivdiv4  30582  ablonnncan1  30585  vccl  30591  nvgcl  30648  nvcom  30649  nvadd4  30653  nvscl  30654  nvmval  30670  nvmcl  30674  nmcvcn  30723  nmlnoubi  30824  isblo3i  30829  blometi  30831  dipsubdir  30876  hlpar2  30924  hlpar  30925  hlcom  30928  hlipcj  30939  hlipgt0  30942  his52  31115  shintcli  31357  chlub  31537  homulass  31830  adjadj  31964  nmophmi  32059  kbass6  32149  atcvatlem  32413  mdsymlem3  32433  mdsymlem5  32435  suppiniseg  32700  rexdiv  32892  tlt3  32944  toslublem  32946  tosglblem  32948  archiabllem1b  33181  archiabllem2  33186  slmdacl  33197  slmdmcl  33198  slmdvacl  33200  lidlincl  33437  cringm4  33453  evls1fldgencl  33694  aean  34224  fiunelcarsg  34297  probcun  34399  probdif  34401  cndprobin  34415  f1resrcmplf1dlem  35078  cusgredgex  35105  swrdwlk  35110  satefvfmla1  35409  climuzcnv  35655  pibt2  37399  matunitlindflem1  37602  mblfinlem1  37643  mblfinlem2  37644  ftc1anclem6  37684  ssbnd  37774  heibor1  37796  exidcl  37862  rngocl  37887  rngogcl  37898  rngocom  37899  rngoa4  37902  rngosub  37916  rngonegmn1l  37927  rngonegmn1r  37928  ispridlc  38056  lshpcmp  38969  opltcon3b  39185  oldmm1  39198  olj01  39206  latm32  39212  omllaw4  39227  omllaw5N  39228  cmtcomlemN  39229  cmt2N  39231  cmtbr2N  39234  cmtbr3N  39235  cmtbr4N  39236  glbconxN  39360  hlexch1  39364  hlexch2  39365  hlexchb1  39366  hlexchb2  39367  hlexch3  39373  hlexch4N  39374  hlatexchb1  39375  hlatexchb2  39376  hlatexch1  39377  hlatexch2  39378  hlatle  39380  hlateq  39381  hlrelat1  39382  hlrelat2  39385  cvr1  39392  cvrval5  39397  cvrp  39398  atcvr1  39399  atcvr2  39400  cvrexchlem  39401  cvrexch  39402  dalem54  39708  pmaple  39743  pmap11  39744  paddass  39820  pmapj2N  39911  pmapocjN  39912  trlval2  40145  nnproddivdvdsd  41981  fsuppssind  42579  mhphf  42583  0prjspnlem  42609  grumnudlem  44280  eelT00  44702  eelTTT  44703  eelT11  44704  eelT12  44706  eelTT1  44707  eelT01  44708  mullimc  45571  mullimcf  45578  dvmptfprod  45900  stoweidlem52  46007  stoweidlem60  46015  focofob  47029  f1ocof1ob  47030  clnbgrgrim  47839  ply1mulgsum  48235  itschlc0xyqsol1  48615  sinhpcosh  48970  reseccl  48983  recsccl  48984  recotcl  48985  onetansqsecsq  48991