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  5615  tz7.5  6335  f1cdmsn  7225  f1ofvswap  7249  f1ofveu  7349  fovcdmda  7526  suppvalfng  8106  smoiso  8291  odi  8503  nndi  8547  nnmsucr  8549  f1oen2g  8901  f1dom2g  8902  domssex2  9061  dif1ennn  9083  enfii  9106  phplem2  9125  php  9127  php3  9129  findcard3  9178  ordunifi  9185  nnsdomg  9194  ackbij1lem16  10136  divneg  11824  divdiv32  11840  divneg2  11856  ltdiv2  12019  fimaxre  12077  fiminre  12080  suprzcl  12563  peano2uz  12805  infssuzle  12835  lbzbi  12840  zbtwnre  12850  irrmul  12878  supxrunb1  13225  expnlbnd  14147  hash1to3  14406  fun2dmnop  14419  brfi1uzind  14422  brcnvtrclfvcnv  14919  retancl  16058  tanneg  16064  demoivreALT  16117  dvdscmulr  16202  dvdsmulcr  16203  mulmoddvds  16248  gcd0id  16437  euclemma  16631  phiprmpw  16694  fermltl  16702  vdwapun  16893  vdwapid1  16894  cshwshashlem1  17014  fsets  17087  pospo  18257  tltnle  18334  latasymb  18356  sgrpcl  18642  mndcl  18658  imasmnd2  18690  gsumsgrpccat  18756  grpcl  18862  dfgrp2  18883  grprcan  18894  grpsubcl  18941  imasgrp2  18976  mhmid  18984  mhmmnd  18985  mulginvcom  19020  mulgnndir  19024  mulgnnass  19030  qusgrp  19106  ghmmulg  19148  ghmrn  19149  ghmeqker  19163  gsumccatsymgsn  19346  ablcom  19719  ablinvadd  19727  mulgmhm  19747  mulgghm  19748  ghmcmn  19751  odadd1  19768  odadd2  19769  rngacl  20088  rngcl  20090  rngpropd  20100  srgcl  20119  srgacl  20131  srgcom  20132  ringcl  20176  crngcom  20177  ringacl  20204  pwspjmhmmgpd  20254  imasring  20257  irredlmul  20355  rhmmul  20412  subrngacl  20480  subrgacl  20507  subrgmcl  20508  subrgugrp  20515  isdomn4  20640  drngmclOLD  20675  isdrngd  20689  isdrngdOLD  20691  srngadd  20775  srngmul  20776  idsrngd  20780  lmodacl  20814  lmodmcl  20815  lmodvacl  20817  lmodvsubcl  20849  lmod4  20854  lmodvaddsub4  20856  lmodvpncan  20857  lmodvnpcan  20858  lmodsubeq0  20863  pwssplit3  21004  islbs2  21100  islbs3  21101  lbsext  21109  rspssp  21185  nzerooringczr  21426  zlmlmod  21468  psgnco  21529  ipdir  21585  ip2eq  21599  ocvin  21620  frlmsplit2  21719  ascldimul  21835  rnasclmulcl  21841  mplbas2  21988  coe1add  22197  coe1subfv  22199  coe1mul2  22202  rhmply1vsca  22323  ringvcl  22335  cramer  22626  chpmat1d  22771  filin  23789  filfinnfr  23812  filuni  23820  ufprim  23844  uffinfix  23862  hausflf  23932  uffcfflf  23974  cnextcn  24002  tmdmulg  24027  tsmsxplem1  24088  psmetcl  24242  xmetcl  24266  metcl  24267  meteq0  24274  metge0  24280  metsym  24285  metgt0  24294  blelrnps  24351  blelrn  24352  blssm  24353  blres  24366  mscl  24396  xmscl  24397  xmsge0  24398  xmseq0  24399  xmssym  24400  mopnin  24432  nmf2  24528  ngpdsr  24540  ngpds2  24541  ngpds2r  24542  ngpds3  24543  ngpds3r  24544  nmge0  24552  nmeq0  24553  nm2dif  24560  nmmul  24599  nlmmul0or  24618  nmods  24679  clmsub  25027  clmacl  25031  clmmcl  25032  clmsubcl  25033  clmvscl  25035  clmvsubval  25056  ncvsprp  25099  ncvsdif  25102  ncvspds  25108  cphnmvs  25137  cphipcl  25138  cphipcj  25146  cphorthcom  25148  cphipval2  25188  4cphipval2  25189  cphipval  25190  fmcfil  25219  mbfi1fseqlem3  25665  mbfi1fseqlem4  25666  mbfi1fseqlem5  25667  deg1ldgdomn  26046  drnguc1p  26126  quotval  26247  sincosq1sgn  26454  sincosq2sgn  26455  sincosq3sgn  26456  sincosq4sgn  26457  efabl  26506  lgsneg1  27280  dchrisumlem3  27449  bdayn0p1  28314  ax5seglem2  28928  usgredg2vtx  29218  uspgredg2vtxeu  29219  usgredg2vtxeu  29220  cplgr3v  29434  vtxdumgr0nedg  29493  clwlkclwwlk  30003  frgrncvvdeqlem8  30307  grpocl  30501  grpodivcl  30540  ablomuldiv  30553  ablodivdiv4  30555  ablonnncan1  30558  vccl  30564  nvgcl  30621  nvcom  30622  nvadd4  30626  nvscl  30627  nvmval  30643  nvmcl  30647  nmcvcn  30696  nmlnoubi  30797  isblo3i  30802  blometi  30804  dipsubdir  30849  hlpar2  30897  hlpar  30898  hlcom  30901  hlipcj  30912  hlipgt0  30915  his52  31088  shintcli  31330  chlub  31510  homulass  31803  adjadj  31937  nmophmi  32032  kbass6  32122  atcvatlem  32386  mdsymlem3  32406  mdsymlem5  32408  suppiniseg  32691  rexdiv  32935  tlt3  32980  toslublem  32982  tosglblem  32984  archiabllem1b  33202  archiabllem2  33207  slmdacl  33219  slmdmcl  33220  slmdvacl  33222  lidlincl  33439  cringm4  33455  evls1fldgencl  33755  aean  34329  fiunelcarsg  34401  probcun  34503  probdif  34505  cndprobin  34519  f1resrcmplf1dlem  35170  rankfilimbi  35184  cusgredgex  35238  swrdwlk  35243  satefvfmla1  35541  climuzcnv  35787  pibt2  37534  matunitlindflem1  37729  mblfinlem1  37770  mblfinlem2  37771  ftc1anclem6  37811  ssbnd  37901  heibor1  37923  exidcl  37989  rngocl  38014  rngogcl  38025  rngocom  38026  rngoa4  38029  rngosub  38043  rngonegmn1l  38054  rngonegmn1r  38055  ispridlc  38183  lshpcmp  39160  opltcon3b  39376  oldmm1  39389  olj01  39397  latm32  39403  omllaw4  39418  omllaw5N  39419  cmtcomlemN  39420  cmt2N  39422  cmtbr2N  39425  cmtbr3N  39426  cmtbr4N  39427  glbconxN  39550  hlexch1  39554  hlexch2  39555  hlexchb1  39556  hlexchb2  39557  hlexch3  39563  hlexch4N  39564  hlatexchb1  39565  hlatexchb2  39566  hlatexch1  39567  hlatexch2  39568  hlatle  39570  hlateq  39571  hlrelat1  39572  hlrelat2  39575  cvr1  39582  cvrval5  39587  cvrp  39588  atcvr1  39589  atcvr2  39590  cvrexchlem  39591  cvrexch  39592  dalem54  39898  pmaple  39933  pmap11  39934  paddass  40010  pmapj2N  40101  pmapocjN  40102  trlval2  40335  nnproddivdvdsd  42166  fsuppssind  42751  mhphf  42755  0prjspnlem  42781  grumnudlem  44442  eelT00  44861  eelTTT  44862  eelT11  44863  eelT12  44865  eelTT1  44866  eelT01  44867  mullimc  45778  mullimcf  45785  dvmptfprod  46105  stoweidlem52  46212  stoweidlem60  46220  focofob  47242  f1ocof1ob  47243  clnbgrgrim  48096  ply1mulgsum  48552  itschlc0xyqsol1  48928  sinhpcosh  49901  reseccl  49914  recsccl  49915  recotcl  49916  onetansqsecsq  49922