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  1178  3adant1r  1179  syl3an1b  1406  syl3an1br  1409  wefrc  5618  tz7.5  6338  f1cdmsn  7230  f1ofvswap  7254  f1ofveu  7354  fovcdmda  7531  suppvalfng  8110  smoiso  8295  odi  8507  nndi  8552  nnmsucr  8554  f1oen2g  8908  f1dom2g  8909  domssex2  9068  dif1ennn  9090  enfii  9113  phplem2  9132  php  9134  php3  9136  findcard3  9186  ordunifi  9193  nnsdomg  9202  ackbij1lem16  10147  divneg  11837  divdiv32  11854  divneg2  11870  ltdiv2  12033  fimaxre  12091  fiminre  12094  suprzcl  12600  peano2uz  12842  infssuzle  12872  lbzbi  12877  zbtwnre  12887  irrmul  12915  supxrunb1  13262  expnlbnd  14186  hash1to3  14445  fun2dmnop  14458  brfi1uzind  14461  brcnvtrclfvcnv  14958  retancl  16100  tanneg  16106  demoivreALT  16159  dvdscmulr  16244  dvdsmulcr  16245  mulmoddvds  16290  gcd0id  16479  euclemma  16674  phiprmpw  16737  fermltl  16745  vdwapun  16936  vdwapid1  16937  cshwshashlem1  17057  fsets  17130  pospo  18300  tltnle  18377  latasymb  18399  sgrpcl  18685  mndcl  18701  imasmnd2  18733  gsumsgrpccat  18799  grpcl  18908  dfgrp2  18929  grprcan  18940  grpsubcl  18987  imasgrp2  19022  mhmid  19030  mhmmnd  19031  mulginvcom  19066  mulgnndir  19070  mulgnnass  19076  qusgrp  19152  ghmmulg  19194  ghmrn  19195  ghmeqker  19209  gsumccatsymgsn  19392  ablcom  19765  ablinvadd  19773  mulgmhm  19793  mulgghm  19794  ghmcmn  19797  odadd1  19814  odadd2  19815  rngacl  20134  rngcl  20136  rngpropd  20146  srgcl  20165  srgacl  20177  srgcom  20178  ringcl  20222  crngcom  20223  ringacl  20250  pwspjmhmmgpd  20298  imasring  20301  irredlmul  20399  rhmmul  20456  subrngacl  20524  subrgacl  20551  subrgmcl  20552  subrgugrp  20559  isdomn4  20684  drngmclOLD  20719  isdrngd  20733  isdrngdOLD  20735  srngadd  20819  srngmul  20820  idsrngd  20824  lmodacl  20858  lmodmcl  20859  lmodvacl  20861  lmodvsubcl  20893  lmod4  20898  lmodvaddsub4  20900  lmodvpncan  20901  lmodvnpcan  20902  lmodsubeq0  20907  pwssplit3  21048  islbs2  21144  islbs3  21145  lbsext  21153  rspssp  21229  nzerooringczr  21470  zlmlmod  21512  psgnco  21573  ipdir  21629  ip2eq  21643  ocvin  21664  frlmsplit2  21763  ascldimul  21878  rnasclmulcl  21884  mplbas2  22030  coe1add  22239  coe1subfv  22241  coe1mul2  22244  rhmply1vsca  22363  ringvcl  22375  cramer  22666  chpmat1d  22811  filin  23829  filfinnfr  23852  filuni  23860  ufprim  23884  uffinfix  23902  hausflf  23972  uffcfflf  24014  cnextcn  24042  tmdmulg  24067  tsmsxplem1  24128  psmetcl  24282  xmetcl  24306  metcl  24307  meteq0  24314  metge0  24320  metsym  24325  metgt0  24334  blelrnps  24391  blelrn  24392  blssm  24393  blres  24406  mscl  24436  xmscl  24437  xmsge0  24438  xmseq0  24439  xmssym  24440  mopnin  24472  nmf2  24568  ngpdsr  24580  ngpds2  24581  ngpds2r  24582  ngpds3  24583  ngpds3r  24584  nmge0  24592  nmeq0  24593  nm2dif  24600  nmmul  24639  nlmmul0or  24658  nmods  24719  clmsub  25057  clmacl  25061  clmmcl  25062  clmsubcl  25063  clmvscl  25065  clmvsubval  25086  ncvsprp  25129  ncvsdif  25132  ncvspds  25138  cphnmvs  25167  cphipcl  25168  cphipcj  25176  cphorthcom  25178  cphipval2  25218  4cphipval2  25219  cphipval  25220  fmcfil  25249  mbfi1fseqlem3  25694  mbfi1fseqlem4  25695  mbfi1fseqlem5  25696  deg1ldgdomn  26069  drnguc1p  26149  quotval  26269  sincosq1sgn  26475  sincosq2sgn  26476  sincosq3sgn  26477  sincosq4sgn  26478  efabl  26527  lgsneg1  27299  dchrisumlem3  27468  bdayn0p1  28375  ax5seglem2  29012  usgredg2vtx  29302  uspgredg2vtxeu  29303  usgredg2vtxeu  29304  cplgr3v  29518  vtxdumgr0nedg  29577  clwlkclwwlk  30087  frgrncvvdeqlem8  30391  grpocl  30586  grpodivcl  30625  ablomuldiv  30638  ablodivdiv4  30640  ablonnncan1  30643  vccl  30649  nvgcl  30706  nvcom  30707  nvadd4  30711  nvscl  30712  nvmval  30728  nvmcl  30732  nmcvcn  30781  nmlnoubi  30882  isblo3i  30887  blometi  30889  dipsubdir  30934  hlpar2  30982  hlpar  30983  hlcom  30986  hlipcj  30997  hlipgt0  31000  his52  31173  shintcli  31415  chlub  31595  homulass  31888  adjadj  32022  nmophmi  32117  kbass6  32207  atcvatlem  32471  mdsymlem3  32491  mdsymlem5  32493  suppiniseg  32774  rexdiv  33000  tlt3  33045  toslublem  33047  tosglblem  33049  archiabllem1b  33268  archiabllem2  33273  slmdacl  33285  slmdmcl  33286  slmdvacl  33288  lidlincl  33505  cringm4  33521  evls1fldgencl  33830  aean  34404  fiunelcarsg  34476  probcun  34578  probdif  34580  cndprobin  34594  f1resrcmplf1dlem  35245  rankfilimbi  35260  cusgredgex  35320  swrdwlk  35325  satefvfmla1  35623  climuzcnv  35869  pibt2  37747  matunitlindflem1  37951  mblfinlem1  37992  mblfinlem2  37993  ftc1anclem6  38033  ssbnd  38123  heibor1  38145  exidcl  38211  rngocl  38236  rngogcl  38247  rngocom  38248  rngoa4  38251  rngosub  38265  rngonegmn1l  38276  rngonegmn1r  38277  ispridlc  38405  lshpcmp  39448  opltcon3b  39664  oldmm1  39677  olj01  39685  latm32  39691  omllaw4  39706  omllaw5N  39707  cmtcomlemN  39708  cmt2N  39710  cmtbr2N  39713  cmtbr3N  39714  cmtbr4N  39715  glbconxN  39838  hlexch1  39842  hlexch2  39843  hlexchb1  39844  hlexchb2  39845  hlexch3  39851  hlexch4N  39852  hlatexchb1  39853  hlatexchb2  39854  hlatexch1  39855  hlatexch2  39856  hlatle  39858  hlateq  39859  hlrelat1  39860  hlrelat2  39863  cvr1  39870  cvrval5  39875  cvrp  39876  atcvr1  39877  atcvr2  39878  cvrexchlem  39879  cvrexch  39880  dalem54  40186  pmaple  40221  pmap11  40222  paddass  40298  pmapj2N  40389  pmapocjN  40390  trlval2  40623  nnproddivdvdsd  42453  fsuppssind  43040  mhphf  43044  0prjspnlem  43070  grumnudlem  44730  eelT00  45149  eelTTT  45150  eelT11  45151  eelT12  45153  eelTT1  45154  eelT01  45155  mullimc  46064  mullimcf  46071  dvmptfprod  46391  stoweidlem52  46498  stoweidlem60  46506  focofob  47540  f1ocof1ob  47541  clnbgrgrim  48422  ply1mulgsum  48878  itschlc0xyqsol1  49254  sinhpcosh  50227  reseccl  50240  recsccl  50241  recotcl  50242  onetansqsecsq  50248