Theorem syl3an1 1156

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

Syntax hints:   → wi 4   ∧ w3a 1080

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 1082

This theorem is referenced by:  3adant1l  1169  3adant1r  1170  syl3an1b  1396  syl3an1br  1399  wefrc  5437  tz7.5  6087  f1ofveu  7011  fovrnda  7175  smoiso  7851  odi  8055  nndi  8099  nnmsucr  8101  f1oen2g  8374  f1dom2g  8375  domssex2  8524  ordunifi  8614  wemappo  8859  wemapso  8861  ackbij1lem16  9503  divneg  11180  divdiv32  11196  divneg2  11212  ltdiv2  11374  fimaxre  11432  fimaxreOLD  11433  fiminre  11436  suprzcl  11911  peano2uz  12150  infssuzle  12180  lbzbi  12185  zbtwnre  12195  irrmul  12223  supxrunb1  12562  expnlbnd  13444  hash1to3  13695  fun2dmnop  13699  brfi1uzind  13702  brcnvtrclfvcnv  14199  retancl  15328  tanneg  15334  demoivreALT  15387  dvdscmulr  15471  dvdsmulcr  15472  mulmoddvds  15512  gcd0id  15700  euclemma  15886  phiprmpw  15942  fermltl  15950  vdwapun  16139  vdwapid1  16140  cshwshashlem1  16258  fsets  16345  pospo  17412  latasymb  17493  mndcl  17740  imasmnd2  17766  grpcl  17869  dfgrp2  17886  grprcan  17894  grpsubcl  17936  imasgrp2  17971  mhmid  17977  mhmmnd  17978  mulginvcom  18006  mulgnndir  18010  mulgnnass  18016  qusgrp  18088  ghmmulg  18111  ghmrn  18112  ghmeqker  18126  gsumccatsymgsn  18285  ablcom  18650  ablinvadd  18655  mulgmhm  18673  mulgghm  18674  ghmcmn  18677  odadd1  18691  odadd2  18692  srgcl  18952  srgacl  18964  srgcom  18965  ringcl  19001  crngcom  19002  ringacl  19018  imasring  19059  irredlmul  19148  rhmmul  19169  drngmcl  19205  isdrngd  19217  subrgacl  19236  subrgugrp  19244  srngadd  19318  srngmul  19319  idsrngd  19323  lmodacl  19335  lmodmcl  19336  lmodvacl  19338  lmodvsubcl  19369  lmod4  19374  lmodvaddsub4  19376  lmodvpncan  19377  lmodvnpcan  19378  lmodsubeq0  19383  pwssplit3  19523  islbs2  19616  islbs3  19617  lbsext  19625  rspssp  19688  ascldimul  19804  ascldimulOLD  19805  rnasclmulcl  19810  mplbas2  19938  coe1add  20115  coe1subfv  20117  coe1mul2  20120  zlmlmod  20352  psgnco  20409  ipdir  20465  ip2eq  20479  ocvin  20500  frlmsplit2  20599  ringvcl  20691  cramer  20984  chpmat1d  21128  filin  22146  filfinnfr  22169  filuni  22177  ufprim  22201  uffinfix  22219  hausflf  22289  uffcfflf  22331  cnextcn  22359  tmdmulg  22384  tsmsxplem1  22444  psmetcl  22600  xmetcl  22624  metcl  22625  meteq0  22632  metge0  22638  metsym  22643  metgt0  22652  blelrnps  22709  blelrn  22710  blssm  22711  blres  22724  mscl  22754  xmscl  22755  xmsge0  22756  xmseq0  22757  xmssym  22758  mopnin  22790  nmf2  22885  ngpdsr  22897  ngpds2  22898  ngpds2r  22899  ngpds3  22900  ngpds3r  22901  nmge0  22909  nmeq0  22910  nm2dif  22917  nmmul  22956  nlmmul0or  22975  nmods  23036  clmsub  23367  clmacl  23371  clmmcl  23372  clmsubcl  23373  clmvscl  23375  clmvsubval  23396  ncvsprp  23439  ncvsdif  23442  ncvspds  23448  cphnmvs  23477  cphipcl  23478  cphipcj  23486  cphorthcom  23488  cphipval2  23527  4cphipval2  23528  cphipval  23529  fmcfil  23558  mbfi1fseqlem3  24001  mbfi1fseqlem4  24002  mbfi1fseqlem5  24003  deg1ldgdomn  24371  drnguc1p  24447  quotval  24564  sincosq1sgn  24767  sincosq2sgn  24768  sincosq3sgn  24769  sincosq4sgn  24770  efabl  24815  lgsneg1  25580  dchrisumlem3  25749  ax5seglem2  26398  usgredg2vtx  26684  uspgredg2vtxeu  26685  usgredg2vtxeu  26686  cplgr3v  26900  vtxdumgr0nedg  26958  clwlkclwwlk  27467  frgrncvvdeqlem8  27777  grpocl  27968  grpodivcl  28007  ablomuldiv  28020  ablodivdiv4  28022  ablonnncan1  28025  vccl  28031  nvgcl  28088  nvcom  28089  nvadd4  28093  nvscl  28094  nvmval  28110  nvmcl  28114  nmcvcn  28163  nmlnoubi  28264  isblo3i  28269  blometi  28271  dipsubdir  28316  hlpar2  28364  hlpar  28365  hlcom  28368  hlipcj  28379  hlipgt0  28382  his52  28555  shintcli  28797  chlub  28977  homulass  29270  adjadj  29404  nmophmi  29499  kbass6  29589  atcvatlem  29853  mdsymlem3  29873  mdsymlem5  29875  rexdiv  30286  tltnle  30323  tlt3  30326  toslublem  30328  tosglblem  30330  archiabllem1b  30459  archiabllem2  30464  slmdacl  30475  slmdmcl  30476  slmdvacl  30478  qusscaval  30575  aean  31120  fiunelcarsg  31191  probcun  31293  probdif  31295  cndprobin  31309  f1resrcmplf1dlem  31973  cusgredgex  31980  satefvfmla1  32280  climuzcnv  32522  pibt2  34229  matunitlindflem1  34419  mblfinlem1  34460  mblfinlem2  34461  ftc1anclem6  34503  ssbnd  34598  heibor1  34620  exidcl  34686  rngocl  34711  rngogcl  34722  rngocom  34723  rngoa4  34726  rngosub  34740  rngonegmn1l  34751  rngonegmn1r  34752  ispridlc  34880  lshpcmp  35655  opltcon3b  35871  oldmm1  35884  olj01  35892  latm32  35898  omllaw4  35913  omllaw5N  35914  cmtcomlemN  35915  cmt2N  35917  cmtbr2N  35920  cmtbr3N  35921  cmtbr4N  35922  glbconxN  36045  hlexch1  36049  hlexch2  36050  hlexchb1  36051  hlexchb2  36052  hlexch3  36058  hlexch4N  36059  hlatexchb1  36060  hlatexchb2  36061  hlatexch1  36062  hlatexch2  36063  hlatle  36065  hlateq  36066  hlrelat1  36067  hlrelat2  36070  cvr1  36077  cvrval5  36082  cvrp  36083  atcvr1  36084  atcvr2  36085  cvrexchlem  36086  cvrexch  36087  dalem54  36393  pmaple  36428  pmap11  36429  paddass  36505  pmapj2N  36596  pmapocjN  36597  trlval2  36830  0prjspnlem  38765  grumnudlem  40118  eelT00  40578  eelTTT  40579  eelT11  40580  eelT12  40582  eelTT1  40583  eelT01  40584  mullimc  41439  mullimcf  41446  stoweidlem52  41879  stoweidlem60  41887  rngcl  43632  nzerooringczr  43821  ply1mulgsum  43924  itschlc0xyqsol1  44234  sinhpcosh  44319  reseccl  44332  recsccl  44333  recotcl  44334  onetansqsecsq  44340