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 1087

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 1089

This theorem is referenced by:  3adant1l  1177  3adant1r  1178  syl3an1b  1405  syl3an1br  1408  wefrc  5679  tz7.5  6405  f1cdmsn  7302  f1ofvswap  7326  f1ofveu  7425  fovcdmda  7604  suppvalfng  8192  smoiso  8402  odi  8617  nndi  8661  nnmsucr  8663  f1oen2g  9009  f1dom2g  9010  domssex2  9177  dif1ennn  9201  enfii  9226  phplem2  9245  php  9247  php3  9249  findcard3  9318  ordunifi  9326  nnsdomg  9335  ackbij1lem16  10274  divneg  11959  divdiv32  11975  divneg2  11991  ltdiv2  12154  fimaxre  12212  fiminre  12215  suprzcl  12698  peano2uz  12943  infssuzle  12973  lbzbi  12978  zbtwnre  12988  irrmul  13016  supxrunb1  13361  expnlbnd  14272  hash1to3  14531  fun2dmnop  14544  brfi1uzind  14547  brcnvtrclfvcnv  15044  retancl  16178  tanneg  16184  demoivreALT  16237  dvdscmulr  16322  dvdsmulcr  16323  mulmoddvds  16367  gcd0id  16556  euclemma  16750  phiprmpw  16813  fermltl  16821  vdwapun  17012  vdwapid1  17013  cshwshashlem1  17133  fsets  17206  pospo  18390  tltnle  18467  latasymb  18487  sgrpcl  18739  mndcl  18755  imasmnd2  18787  gsumsgrpccat  18853  grpcl  18959  dfgrp2  18980  grprcan  18991  grpsubcl  19038  imasgrp2  19073  mhmid  19081  mhmmnd  19082  mulginvcom  19117  mulgnndir  19121  mulgnnass  19127  qusgrp  19204  ghmmulg  19246  ghmrn  19247  ghmeqker  19261  gsumccatsymgsn  19444  ablcom  19817  ablinvadd  19825  mulgmhm  19845  mulgghm  19846  ghmcmn  19849  odadd1  19866  odadd2  19867  rngacl  20159  rngcl  20161  rngpropd  20171  srgcl  20190  srgacl  20202  srgcom  20203  ringcl  20247  crngcom  20248  ringacl  20275  pwspjmhmmgpd  20325  imasring  20327  irredlmul  20428  rhmmul  20486  subrngacl  20556  subrgacl  20583  subrgmcl  20584  subrgugrp  20591  isdomn4  20716  drngmclOLD  20751  isdrngd  20765  isdrngdOLD  20767  srngadd  20852  srngmul  20853  idsrngd  20857  lmodacl  20870  lmodmcl  20871  lmodvacl  20873  lmodvsubcl  20905  lmod4  20910  lmodvaddsub4  20912  lmodvpncan  20913  lmodvnpcan  20914  lmodsubeq0  20919  pwssplit3  21060  islbs2  21156  islbs3  21157  lbsext  21165  rspssp  21249  nzerooringczr  21491  zlmlmod  21537  psgnco  21601  ipdir  21657  ip2eq  21671  ocvin  21692  frlmsplit2  21793  ascldimul  21908  rnasclmulcl  21914  mplbas2  22060  coe1add  22267  coe1subfv  22269  coe1mul2  22272  rhmply1vsca  22392  ringvcl  22404  cramer  22697  chpmat1d  22842  filin  23862  filfinnfr  23885  filuni  23893  ufprim  23917  uffinfix  23935  hausflf  24005  uffcfflf  24047  cnextcn  24075  tmdmulg  24100  tsmsxplem1  24161  psmetcl  24317  xmetcl  24341  metcl  24342  meteq0  24349  metge0  24355  metsym  24360  metgt0  24369  blelrnps  24426  blelrn  24427  blssm  24428  blres  24441  mscl  24471  xmscl  24472  xmsge0  24473  xmseq0  24474  xmssym  24475  mopnin  24510  nmf2  24606  ngpdsr  24618  ngpds2  24619  ngpds2r  24620  ngpds3  24621  ngpds3r  24622  nmge0  24630  nmeq0  24631  nm2dif  24638  nmmul  24685  nlmmul0or  24704  nmods  24765  clmsub  25113  clmacl  25117  clmmcl  25118  clmsubcl  25119  clmvscl  25121  clmvsubval  25142  ncvsprp  25186  ncvsdif  25189  ncvspds  25195  cphnmvs  25224  cphipcl  25225  cphipcj  25233  cphorthcom  25235  cphipval2  25275  4cphipval2  25276  cphipval  25277  fmcfil  25306  mbfi1fseqlem3  25752  mbfi1fseqlem4  25753  mbfi1fseqlem5  25754  deg1ldgdomn  26133  drnguc1p  26213  quotval  26334  sincosq1sgn  26540  sincosq2sgn  26541  sincosq3sgn  26542  sincosq4sgn  26543  efabl  26592  lgsneg1  27366  dchrisumlem3  27535  ax5seglem2  28944  usgredg2vtx  29236  uspgredg2vtxeu  29237  usgredg2vtxeu  29238  cplgr3v  29452  vtxdumgr0nedg  29511  clwlkclwwlk  30021  frgrncvvdeqlem8  30325  grpocl  30519  grpodivcl  30558  ablomuldiv  30571  ablodivdiv4  30573  ablonnncan1  30576  vccl  30582  nvgcl  30639  nvcom  30640  nvadd4  30644  nvscl  30645  nvmval  30661  nvmcl  30665  nmcvcn  30714  nmlnoubi  30815  isblo3i  30820  blometi  30822  dipsubdir  30867  hlpar2  30915  hlpar  30916  hlcom  30919  hlipcj  30930  hlipgt0  30933  his52  31106  shintcli  31348  chlub  31528  homulass  31821  adjadj  31955  nmophmi  32050  kbass6  32140  atcvatlem  32404  mdsymlem3  32424  mdsymlem5  32426  suppiniseg  32695  rexdiv  32908  tlt3  32960  toslublem  32962  tosglblem  32964  archiabllem1b  33199  archiabllem2  33204  slmdacl  33215  slmdmcl  33216  slmdvacl  33218  lidlincl  33458  cringm4  33474  evls1fldgencl  33720  aean  34245  fiunelcarsg  34318  probcun  34420  probdif  34422  cndprobin  34436  f1resrcmplf1dlem  35100  cusgredgex  35127  swrdwlk  35132  satefvfmla1  35430  climuzcnv  35676  pibt2  37418  matunitlindflem1  37623  mblfinlem1  37664  mblfinlem2  37665  ftc1anclem6  37705  ssbnd  37795  heibor1  37817  exidcl  37883  rngocl  37908  rngogcl  37919  rngocom  37920  rngoa4  37923  rngosub  37937  rngonegmn1l  37948  rngonegmn1r  37949  ispridlc  38077  lshpcmp  38989  opltcon3b  39205  oldmm1  39218  olj01  39226  latm32  39232  omllaw4  39247  omllaw5N  39248  cmtcomlemN  39249  cmt2N  39251  cmtbr2N  39254  cmtbr3N  39255  cmtbr4N  39256  glbconxN  39380  hlexch1  39384  hlexch2  39385  hlexchb1  39386  hlexchb2  39387  hlexch3  39393  hlexch4N  39394  hlatexchb1  39395  hlatexchb2  39396  hlatexch1  39397  hlatexch2  39398  hlatle  39400  hlateq  39401  hlrelat1  39402  hlrelat2  39405  cvr1  39412  cvrval5  39417  cvrp  39418  atcvr1  39419  atcvr2  39420  cvrexchlem  39421  cvrexch  39422  dalem54  39728  pmaple  39763  pmap11  39764  paddass  39840  pmapj2N  39931  pmapocjN  39932  trlval2  40165  nnproddivdvdsd  42001  fsuppssind  42603  mhphf  42607  0prjspnlem  42633  grumnudlem  44304  eelT00  44725  eelTTT  44726  eelT11  44727  eelT12  44729  eelTT1  44730  eelT01  44731  mullimc  45631  mullimcf  45638  dvmptfprod  45960  stoweidlem52  46067  stoweidlem60  46075  focofob  47092  f1ocof1ob  47093  clnbgrgrim  47902  ply1mulgsum  48307  itschlc0xyqsol1  48687  sinhpcosh  49259  reseccl  49272  recsccl  49273  recotcl  49274  onetansqsecsq  49280