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  5618  tz7.5  6338  f1cdmsn  7228  f1ofvswap  7252  f1ofveu  7352  fovcdmda  7529  suppvalfng  8109  smoiso  8294  odi  8506  nndi  8551  nnmsucr  8553  f1oen2g  8905  f1dom2g  8906  domssex2  9065  dif1ennn  9087  enfii  9110  phplem2  9129  php  9131  php3  9133  findcard3  9183  ordunifi  9190  nnsdomg  9199  ackbij1lem16  10144  divneg  11833  divdiv32  11849  divneg2  11865  ltdiv2  12028  fimaxre  12086  fiminre  12089  suprzcl  12572  peano2uz  12814  infssuzle  12844  lbzbi  12849  zbtwnre  12859  irrmul  12887  supxrunb1  13234  expnlbnd  14156  hash1to3  14415  fun2dmnop  14428  brfi1uzind  14431  brcnvtrclfvcnv  14928  retancl  16067  tanneg  16073  demoivreALT  16126  dvdscmulr  16211  dvdsmulcr  16212  mulmoddvds  16257  gcd0id  16446  euclemma  16640  phiprmpw  16703  fermltl  16711  vdwapun  16902  vdwapid1  16903  cshwshashlem1  17023  fsets  17096  pospo  18266  tltnle  18343  latasymb  18365  sgrpcl  18651  mndcl  18667  imasmnd2  18699  gsumsgrpccat  18765  grpcl  18871  dfgrp2  18892  grprcan  18903  grpsubcl  18950  imasgrp2  18985  mhmid  18993  mhmmnd  18994  mulginvcom  19029  mulgnndir  19033  mulgnnass  19039  qusgrp  19115  ghmmulg  19157  ghmrn  19158  ghmeqker  19172  gsumccatsymgsn  19355  ablcom  19728  ablinvadd  19736  mulgmhm  19756  mulgghm  19757  ghmcmn  19760  odadd1  19777  odadd2  19778  rngacl  20097  rngcl  20099  rngpropd  20109  srgcl  20128  srgacl  20140  srgcom  20141  ringcl  20185  crngcom  20186  ringacl  20213  pwspjmhmmgpd  20263  imasring  20266  irredlmul  20364  rhmmul  20421  subrngacl  20489  subrgacl  20516  subrgmcl  20517  subrgugrp  20524  isdomn4  20649  drngmclOLD  20684  isdrngd  20698  isdrngdOLD  20700  srngadd  20784  srngmul  20785  idsrngd  20789  lmodacl  20823  lmodmcl  20824  lmodvacl  20826  lmodvsubcl  20858  lmod4  20863  lmodvaddsub4  20865  lmodvpncan  20866  lmodvnpcan  20867  lmodsubeq0  20872  pwssplit3  21013  islbs2  21109  islbs3  21110  lbsext  21118  rspssp  21194  nzerooringczr  21435  zlmlmod  21477  psgnco  21538  ipdir  21594  ip2eq  21608  ocvin  21629  frlmsplit2  21728  ascldimul  21844  rnasclmulcl  21850  mplbas2  21997  coe1add  22206  coe1subfv  22208  coe1mul2  22211  rhmply1vsca  22332  ringvcl  22344  cramer  22635  chpmat1d  22780  filin  23798  filfinnfr  23821  filuni  23829  ufprim  23853  uffinfix  23871  hausflf  23941  uffcfflf  23983  cnextcn  24011  tmdmulg  24036  tsmsxplem1  24097  psmetcl  24251  xmetcl  24275  metcl  24276  meteq0  24283  metge0  24289  metsym  24294  metgt0  24303  blelrnps  24360  blelrn  24361  blssm  24362  blres  24375  mscl  24405  xmscl  24406  xmsge0  24407  xmseq0  24408  xmssym  24409  mopnin  24441  nmf2  24537  ngpdsr  24549  ngpds2  24550  ngpds2r  24551  ngpds3  24552  ngpds3r  24553  nmge0  24561  nmeq0  24562  nm2dif  24569  nmmul  24608  nlmmul0or  24627  nmods  24688  clmsub  25036  clmacl  25040  clmmcl  25041  clmsubcl  25042  clmvscl  25044  clmvsubval  25065  ncvsprp  25108  ncvsdif  25111  ncvspds  25117  cphnmvs  25146  cphipcl  25147  cphipcj  25155  cphorthcom  25157  cphipval2  25197  4cphipval2  25198  cphipval  25199  fmcfil  25228  mbfi1fseqlem3  25674  mbfi1fseqlem4  25675  mbfi1fseqlem5  25676  deg1ldgdomn  26055  drnguc1p  26135  quotval  26256  sincosq1sgn  26463  sincosq2sgn  26464  sincosq3sgn  26465  sincosq4sgn  26466  efabl  26515  lgsneg1  27289  dchrisumlem3  27458  bdayn0p1  28365  ax5seglem2  29002  usgredg2vtx  29292  uspgredg2vtxeu  29293  usgredg2vtxeu  29294  cplgr3v  29508  vtxdumgr0nedg  29567  clwlkclwwlk  30077  frgrncvvdeqlem8  30381  grpocl  30575  grpodivcl  30614  ablomuldiv  30627  ablodivdiv4  30629  ablonnncan1  30632  vccl  30638  nvgcl  30695  nvcom  30696  nvadd4  30700  nvscl  30701  nvmval  30717  nvmcl  30721  nmcvcn  30770  nmlnoubi  30871  isblo3i  30876  blometi  30878  dipsubdir  30923  hlpar2  30971  hlpar  30972  hlcom  30975  hlipcj  30986  hlipgt0  30989  his52  31162  shintcli  31404  chlub  31584  homulass  31877  adjadj  32011  nmophmi  32106  kbass6  32196  atcvatlem  32460  mdsymlem3  32480  mdsymlem5  32482  suppiniseg  32765  rexdiv  33007  tlt3  33052  toslublem  33054  tosglblem  33056  archiabllem1b  33274  archiabllem2  33279  slmdacl  33291  slmdmcl  33292  slmdvacl  33294  lidlincl  33511  cringm4  33527  evls1fldgencl  33827  aean  34401  fiunelcarsg  34473  probcun  34575  probdif  34577  cndprobin  34591  f1resrcmplf1dlem  35242  rankfilimbi  35257  cusgredgex  35316  swrdwlk  35321  satefvfmla1  35619  climuzcnv  35865  pibt2  37622  matunitlindflem1  37817  mblfinlem1  37858  mblfinlem2  37859  ftc1anclem6  37899  ssbnd  37989  heibor1  38011  exidcl  38077  rngocl  38102  rngogcl  38113  rngocom  38114  rngoa4  38117  rngosub  38131  rngonegmn1l  38142  rngonegmn1r  38143  ispridlc  38271  lshpcmp  39248  opltcon3b  39464  oldmm1  39477  olj01  39485  latm32  39491  omllaw4  39506  omllaw5N  39507  cmtcomlemN  39508  cmt2N  39510  cmtbr2N  39513  cmtbr3N  39514  cmtbr4N  39515  glbconxN  39638  hlexch1  39642  hlexch2  39643  hlexchb1  39644  hlexchb2  39645  hlexch3  39651  hlexch4N  39652  hlatexchb1  39653  hlatexchb2  39654  hlatexch1  39655  hlatexch2  39656  hlatle  39658  hlateq  39659  hlrelat1  39660  hlrelat2  39663  cvr1  39670  cvrval5  39675  cvrp  39676  atcvr1  39677  atcvr2  39678  cvrexchlem  39679  cvrexch  39680  dalem54  39986  pmaple  40021  pmap11  40022  paddass  40098  pmapj2N  40189  pmapocjN  40190  trlval2  40423  nnproddivdvdsd  42254  fsuppssind  42836  mhphf  42840  0prjspnlem  42866  grumnudlem  44526  eelT00  44945  eelTTT  44946  eelT11  44947  eelT12  44949  eelTT1  44950  eelT01  44951  mullimc  45862  mullimcf  45869  dvmptfprod  46189  stoweidlem52  46296  stoweidlem60  46304  focofob  47326  f1ocof1ob  47327  clnbgrgrim  48180  ply1mulgsum  48636  itschlc0xyqsol1  49012  sinhpcosh  49985  reseccl  49998  recsccl  49999  recotcl  50000  onetansqsecsq  50006