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  5625  tz7.5  6341  f1cdmsn  7239  f1ofvswap  7263  f1ofveu  7363  fovcdmda  7540  suppvalfng  8123  smoiso  8308  odi  8520  nndi  8564  nnmsucr  8566  f1oen2g  8917  f1dom2g  8918  domssex2  9078  dif1ennn  9102  enfii  9127  phplem2  9146  php  9148  php3  9150  findcard3  9205  ordunifi  9213  nnsdomg  9222  ackbij1lem16  10163  divneg  11850  divdiv32  11866  divneg2  11882  ltdiv2  12045  fimaxre  12103  fiminre  12106  suprzcl  12590  peano2uz  12836  infssuzle  12866  lbzbi  12871  zbtwnre  12881  irrmul  12909  supxrunb1  13255  expnlbnd  14174  hash1to3  14433  fun2dmnop  14446  brfi1uzind  14449  brcnvtrclfvcnv  14947  retancl  16086  tanneg  16092  demoivreALT  16145  dvdscmulr  16230  dvdsmulcr  16231  mulmoddvds  16276  gcd0id  16465  euclemma  16659  phiprmpw  16722  fermltl  16730  vdwapun  16921  vdwapid1  16922  cshwshashlem1  17042  fsets  17115  pospo  18280  tltnle  18357  latasymb  18377  sgrpcl  18629  mndcl  18645  imasmnd2  18677  gsumsgrpccat  18743  grpcl  18849  dfgrp2  18870  grprcan  18881  grpsubcl  18928  imasgrp2  18963  mhmid  18971  mhmmnd  18972  mulginvcom  19007  mulgnndir  19011  mulgnnass  19017  qusgrp  19094  ghmmulg  19136  ghmrn  19137  ghmeqker  19151  gsumccatsymgsn  19332  ablcom  19705  ablinvadd  19713  mulgmhm  19733  mulgghm  19734  ghmcmn  19737  odadd1  19754  odadd2  19755  rngacl  20047  rngcl  20049  rngpropd  20059  srgcl  20078  srgacl  20090  srgcom  20091  ringcl  20135  crngcom  20136  ringacl  20163  pwspjmhmmgpd  20213  imasring  20215  irredlmul  20313  rhmmul  20371  subrngacl  20441  subrgacl  20468  subrgmcl  20469  subrgugrp  20476  isdomn4  20601  drngmclOLD  20636  isdrngd  20650  isdrngdOLD  20652  srngadd  20736  srngmul  20737  idsrngd  20741  lmodacl  20754  lmodmcl  20755  lmodvacl  20757  lmodvsubcl  20789  lmod4  20794  lmodvaddsub4  20796  lmodvpncan  20797  lmodvnpcan  20798  lmodsubeq0  20803  pwssplit3  20944  islbs2  21040  islbs3  21041  lbsext  21049  rspssp  21125  nzerooringczr  21366  zlmlmod  21408  psgnco  21468  ipdir  21524  ip2eq  21538  ocvin  21559  frlmsplit2  21658  ascldimul  21773  rnasclmulcl  21779  mplbas2  21925  coe1add  22126  coe1subfv  22128  coe1mul2  22131  rhmply1vsca  22251  ringvcl  22263  cramer  22554  chpmat1d  22699  filin  23717  filfinnfr  23740  filuni  23748  ufprim  23772  uffinfix  23790  hausflf  23860  uffcfflf  23902  cnextcn  23930  tmdmulg  23955  tsmsxplem1  24016  psmetcl  24171  xmetcl  24195  metcl  24196  meteq0  24203  metge0  24209  metsym  24214  metgt0  24223  blelrnps  24280  blelrn  24281  blssm  24282  blres  24295  mscl  24325  xmscl  24326  xmsge0  24327  xmseq0  24328  xmssym  24329  mopnin  24361  nmf2  24457  ngpdsr  24469  ngpds2  24470  ngpds2r  24471  ngpds3  24472  ngpds3r  24473  nmge0  24481  nmeq0  24482  nm2dif  24489  nmmul  24528  nlmmul0or  24547  nmods  24608  clmsub  24956  clmacl  24960  clmmcl  24961  clmsubcl  24962  clmvscl  24964  clmvsubval  24985  ncvsprp  25028  ncvsdif  25031  ncvspds  25037  cphnmvs  25066  cphipcl  25067  cphipcj  25075  cphorthcom  25077  cphipval2  25117  4cphipval2  25118  cphipval  25119  fmcfil  25148  mbfi1fseqlem3  25594  mbfi1fseqlem4  25595  mbfi1fseqlem5  25596  deg1ldgdomn  25975  drnguc1p  26055  quotval  26176  sincosq1sgn  26383  sincosq2sgn  26384  sincosq3sgn  26385  sincosq4sgn  26386  efabl  26435  lgsneg1  27209  dchrisumlem3  27378  bdayn0p1  28234  ax5seglem2  28832  usgredg2vtx  29122  uspgredg2vtxeu  29123  usgredg2vtxeu  29124  cplgr3v  29338  vtxdumgr0nedg  29397  clwlkclwwlk  29904  frgrncvvdeqlem8  30208  grpocl  30402  grpodivcl  30441  ablomuldiv  30454  ablodivdiv4  30456  ablonnncan1  30459  vccl  30465  nvgcl  30522  nvcom  30523  nvadd4  30527  nvscl  30528  nvmval  30544  nvmcl  30548  nmcvcn  30597  nmlnoubi  30698  isblo3i  30703  blometi  30705  dipsubdir  30750  hlpar2  30798  hlpar  30799  hlcom  30802  hlipcj  30813  hlipgt0  30816  his52  30989  shintcli  31231  chlub  31411  homulass  31704  adjadj  31838  nmophmi  31933  kbass6  32023  atcvatlem  32287  mdsymlem3  32307  mdsymlem5  32309  suppiniseg  32582  rexdiv  32819  tlt3  32869  toslublem  32871  tosglblem  32873  archiabllem1b  33119  archiabllem2  33124  slmdacl  33135  slmdmcl  33136  slmdvacl  33138  lidlincl  33374  cringm4  33390  evls1fldgencl  33638  aean  34207  fiunelcarsg  34280  probcun  34382  probdif  34384  cndprobin  34398  f1resrcmplf1dlem  35049  cusgredgex  35082  swrdwlk  35087  satefvfmla1  35385  climuzcnv  35631  pibt2  37378  matunitlindflem1  37583  mblfinlem1  37624  mblfinlem2  37625  ftc1anclem6  37665  ssbnd  37755  heibor1  37777  exidcl  37843  rngocl  37868  rngogcl  37879  rngocom  37880  rngoa4  37883  rngosub  37897  rngonegmn1l  37908  rngonegmn1r  37909  ispridlc  38037  lshpcmp  38954  opltcon3b  39170  oldmm1  39183  olj01  39191  latm32  39197  omllaw4  39212  omllaw5N  39213  cmtcomlemN  39214  cmt2N  39216  cmtbr2N  39219  cmtbr3N  39220  cmtbr4N  39221  glbconxN  39345  hlexch1  39349  hlexch2  39350  hlexchb1  39351  hlexchb2  39352  hlexch3  39358  hlexch4N  39359  hlatexchb1  39360  hlatexchb2  39361  hlatexch1  39362  hlatexch2  39363  hlatle  39365  hlateq  39366  hlrelat1  39367  hlrelat2  39370  cvr1  39377  cvrval5  39382  cvrp  39383  atcvr1  39384  atcvr2  39385  cvrexchlem  39386  cvrexch  39387  dalem54  39693  pmaple  39728  pmap11  39729  paddass  39805  pmapj2N  39896  pmapocjN  39897  trlval2  40130  nnproddivdvdsd  41961  fsuppssind  42554  mhphf  42558  0prjspnlem  42584  grumnudlem  44247  eelT00  44667  eelTTT  44668  eelT11  44669  eelT12  44671  eelTT1  44672  eelT01  44673  mullimc  45587  mullimcf  45594  dvmptfprod  45916  stoweidlem52  46023  stoweidlem60  46031  focofob  47054  f1ocof1ob  47055  clnbgrgrim  47907  ply1mulgsum  48352  itschlc0xyqsol1  48728  sinhpcosh  49702  reseccl  49715  recsccl  49716  recotcl  49717  onetansqsecsq  49723