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  5605  tz7.5  6322  f1cdmsn  7211  f1ofvswap  7235  f1ofveu  7335  fovcdmda  7512  suppvalfng  8092  smoiso  8277  odi  8489  nndi  8533  nnmsucr  8535  f1oen2g  8886  f1dom2g  8887  domssex2  9045  dif1ennn  9067  enfii  9090  phplem2  9109  php  9111  php3  9113  findcard3  9162  ordunifi  9169  nnsdomg  9178  ackbij1lem16  10120  divneg  11808  divdiv32  11824  divneg2  11840  ltdiv2  12003  fimaxre  12061  fiminre  12064  suprzcl  12548  peano2uz  12794  infssuzle  12824  lbzbi  12829  zbtwnre  12839  irrmul  12867  supxrunb1  13213  expnlbnd  14135  hash1to3  14394  fun2dmnop  14407  brfi1uzind  14410  brcnvtrclfvcnv  14907  retancl  16046  tanneg  16052  demoivreALT  16105  dvdscmulr  16190  dvdsmulcr  16191  mulmoddvds  16236  gcd0id  16425  euclemma  16619  phiprmpw  16682  fermltl  16690  vdwapun  16881  vdwapid1  16882  cshwshashlem1  17002  fsets  17075  pospo  18244  tltnle  18321  latasymb  18343  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  19093  ghmmulg  19135  ghmrn  19136  ghmeqker  19150  gsumccatsymgsn  19333  ablcom  19706  ablinvadd  19714  mulgmhm  19734  mulgghm  19735  ghmcmn  19738  odadd1  19755  odadd2  19756  rngacl  20075  rngcl  20077  rngpropd  20087  srgcl  20106  srgacl  20118  srgcom  20119  ringcl  20163  crngcom  20164  ringacl  20191  pwspjmhmmgpd  20241  imasring  20243  irredlmul  20341  rhmmul  20398  subrngacl  20466  subrgacl  20493  subrgmcl  20494  subrgugrp  20501  isdomn4  20626  drngmclOLD  20661  isdrngd  20675  isdrngdOLD  20677  srngadd  20761  srngmul  20762  idsrngd  20766  lmodacl  20800  lmodmcl  20801  lmodvacl  20803  lmodvsubcl  20835  lmod4  20840  lmodvaddsub4  20842  lmodvpncan  20843  lmodvnpcan  20844  lmodsubeq0  20849  pwssplit3  20990  islbs2  21086  islbs3  21087  lbsext  21095  rspssp  21171  nzerooringczr  21412  zlmlmod  21454  psgnco  21515  ipdir  21571  ip2eq  21585  ocvin  21606  frlmsplit2  21705  ascldimul  21820  rnasclmulcl  21826  mplbas2  21972  coe1add  22173  coe1subfv  22175  coe1mul2  22178  rhmply1vsca  22298  ringvcl  22310  cramer  22601  chpmat1d  22746  filin  23764  filfinnfr  23787  filuni  23795  ufprim  23819  uffinfix  23837  hausflf  23907  uffcfflf  23949  cnextcn  23977  tmdmulg  24002  tsmsxplem1  24063  psmetcl  24217  xmetcl  24241  metcl  24242  meteq0  24249  metge0  24255  metsym  24260  metgt0  24269  blelrnps  24326  blelrn  24327  blssm  24328  blres  24341  mscl  24371  xmscl  24372  xmsge0  24373  xmseq0  24374  xmssym  24375  mopnin  24407  nmf2  24503  ngpdsr  24515  ngpds2  24516  ngpds2r  24517  ngpds3  24518  ngpds3r  24519  nmge0  24527  nmeq0  24528  nm2dif  24535  nmmul  24574  nlmmul0or  24593  nmods  24654  clmsub  25002  clmacl  25006  clmmcl  25007  clmsubcl  25008  clmvscl  25010  clmvsubval  25031  ncvsprp  25074  ncvsdif  25077  ncvspds  25083  cphnmvs  25112  cphipcl  25113  cphipcj  25121  cphorthcom  25123  cphipval2  25163  4cphipval2  25164  cphipval  25165  fmcfil  25194  mbfi1fseqlem3  25640  mbfi1fseqlem4  25641  mbfi1fseqlem5  25642  deg1ldgdomn  26021  drnguc1p  26101  quotval  26222  sincosq1sgn  26429  sincosq2sgn  26430  sincosq3sgn  26431  sincosq4sgn  26432  efabl  26481  lgsneg1  27255  dchrisumlem3  27424  bdayn0p1  28289  ax5seglem2  28902  usgredg2vtx  29192  uspgredg2vtxeu  29193  usgredg2vtxeu  29194  cplgr3v  29408  vtxdumgr0nedg  29467  clwlkclwwlk  29974  frgrncvvdeqlem8  30278  grpocl  30472  grpodivcl  30511  ablomuldiv  30524  ablodivdiv4  30526  ablonnncan1  30529  vccl  30535  nvgcl  30592  nvcom  30593  nvadd4  30597  nvscl  30598  nvmval  30614  nvmcl  30618  nmcvcn  30667  nmlnoubi  30768  isblo3i  30773  blometi  30775  dipsubdir  30820  hlpar2  30868  hlpar  30869  hlcom  30872  hlipcj  30883  hlipgt0  30886  his52  31059  shintcli  31301  chlub  31481  homulass  31774  adjadj  31908  nmophmi  32003  kbass6  32093  atcvatlem  32357  mdsymlem3  32377  mdsymlem5  32379  suppiniseg  32659  rexdiv  32898  tlt3  32943  toslublem  32945  tosglblem  32947  archiabllem1b  33153  archiabllem2  33158  slmdacl  33170  slmdmcl  33171  slmdvacl  33173  lidlincl  33387  cringm4  33403  evls1fldgencl  33675  aean  34249  fiunelcarsg  34321  probcun  34423  probdif  34425  cndprobin  34439  f1resrcmplf1dlem  35090  rankfilimbi  35104  cusgredgex  35158  swrdwlk  35163  satefvfmla1  35461  climuzcnv  35707  pibt2  37451  matunitlindflem1  37656  mblfinlem1  37697  mblfinlem2  37698  ftc1anclem6  37738  ssbnd  37828  heibor1  37850  exidcl  37916  rngocl  37941  rngogcl  37952  rngocom  37953  rngoa4  37956  rngosub  37970  rngonegmn1l  37981  rngonegmn1r  37982  ispridlc  38110  lshpcmp  39027  opltcon3b  39243  oldmm1  39256  olj01  39264  latm32  39270  omllaw4  39285  omllaw5N  39286  cmtcomlemN  39287  cmt2N  39289  cmtbr2N  39292  cmtbr3N  39293  cmtbr4N  39294  glbconxN  39417  hlexch1  39421  hlexch2  39422  hlexchb1  39423  hlexchb2  39424  hlexch3  39430  hlexch4N  39431  hlatexchb1  39432  hlatexchb2  39433  hlatexch1  39434  hlatexch2  39435  hlatle  39437  hlateq  39438  hlrelat1  39439  hlrelat2  39442  cvr1  39449  cvrval5  39454  cvrp  39455  atcvr1  39456  atcvr2  39457  cvrexchlem  39458  cvrexch  39459  dalem54  39765  pmaple  39800  pmap11  39801  paddass  39877  pmapj2N  39968  pmapocjN  39969  trlval2  40202  nnproddivdvdsd  42033  fsuppssind  42626  mhphf  42630  0prjspnlem  42656  grumnudlem  44318  eelT00  44737  eelTTT  44738  eelT11  44739  eelT12  44741  eelTT1  44742  eelT01  44743  mullimc  45656  mullimcf  45663  dvmptfprod  45983  stoweidlem52  46090  stoweidlem60  46098  focofob  47111  f1ocof1ob  47112  clnbgrgrim  47965  ply1mulgsum  48422  itschlc0xyqsol1  48798  sinhpcosh  49772  reseccl  49785  recsccl  49786  recotcl  49787  onetansqsecsq  49793