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  5626  tz7.5  6346  f1cdmsn  7238  f1ofvswap  7262  f1ofveu  7362  fovcdmda  7539  suppvalfng  8119  smoiso  8304  odi  8516  nndi  8561  nnmsucr  8563  f1oen2g  8917  f1dom2g  8918  domssex2  9077  dif1ennn  9099  enfii  9122  phplem2  9141  php  9143  php3  9145  findcard3  9195  ordunifi  9202  nnsdomg  9211  ackbij1lem16  10156  divneg  11845  divdiv32  11861  divneg2  11877  ltdiv2  12040  fimaxre  12098  fiminre  12101  suprzcl  12584  peano2uz  12826  infssuzle  12856  lbzbi  12861  zbtwnre  12871  irrmul  12899  supxrunb1  13246  expnlbnd  14168  hash1to3  14427  fun2dmnop  14440  brfi1uzind  14443  brcnvtrclfvcnv  14940  retancl  16079  tanneg  16085  demoivreALT  16138  dvdscmulr  16223  dvdsmulcr  16224  mulmoddvds  16269  gcd0id  16458  euclemma  16652  phiprmpw  16715  fermltl  16723  vdwapun  16914  vdwapid1  16915  cshwshashlem1  17035  fsets  17108  pospo  18278  tltnle  18355  latasymb  18377  sgrpcl  18663  mndcl  18679  imasmnd2  18711  gsumsgrpccat  18777  grpcl  18883  dfgrp2  18904  grprcan  18915  grpsubcl  18962  imasgrp2  18997  mhmid  19005  mhmmnd  19006  mulginvcom  19041  mulgnndir  19045  mulgnnass  19051  qusgrp  19127  ghmmulg  19169  ghmrn  19170  ghmeqker  19184  gsumccatsymgsn  19367  ablcom  19740  ablinvadd  19748  mulgmhm  19768  mulgghm  19769  ghmcmn  19772  odadd1  19789  odadd2  19790  rngacl  20109  rngcl  20111  rngpropd  20121  srgcl  20140  srgacl  20152  srgcom  20153  ringcl  20197  crngcom  20198  ringacl  20225  pwspjmhmmgpd  20275  imasring  20278  irredlmul  20376  rhmmul  20433  subrngacl  20501  subrgacl  20528  subrgmcl  20529  subrgugrp  20536  isdomn4  20661  drngmclOLD  20696  isdrngd  20710  isdrngdOLD  20712  srngadd  20796  srngmul  20797  idsrngd  20801  lmodacl  20835  lmodmcl  20836  lmodvacl  20838  lmodvsubcl  20870  lmod4  20875  lmodvaddsub4  20877  lmodvpncan  20878  lmodvnpcan  20879  lmodsubeq0  20884  pwssplit3  21025  islbs2  21121  islbs3  21122  lbsext  21130  rspssp  21206  nzerooringczr  21447  zlmlmod  21489  psgnco  21550  ipdir  21606  ip2eq  21620  ocvin  21641  frlmsplit2  21740  ascldimul  21856  rnasclmulcl  21862  mplbas2  22009  coe1add  22218  coe1subfv  22220  coe1mul2  22223  rhmply1vsca  22344  ringvcl  22356  cramer  22647  chpmat1d  22792  filin  23810  filfinnfr  23833  filuni  23841  ufprim  23865  uffinfix  23883  hausflf  23953  uffcfflf  23995  cnextcn  24023  tmdmulg  24048  tsmsxplem1  24109  psmetcl  24263  xmetcl  24287  metcl  24288  meteq0  24295  metge0  24301  metsym  24306  metgt0  24315  blelrnps  24372  blelrn  24373  blssm  24374  blres  24387  mscl  24417  xmscl  24418  xmsge0  24419  xmseq0  24420  xmssym  24421  mopnin  24453  nmf2  24549  ngpdsr  24561  ngpds2  24562  ngpds2r  24563  ngpds3  24564  ngpds3r  24565  nmge0  24573  nmeq0  24574  nm2dif  24581  nmmul  24620  nlmmul0or  24639  nmods  24700  clmsub  25048  clmacl  25052  clmmcl  25053  clmsubcl  25054  clmvscl  25056  clmvsubval  25077  ncvsprp  25120  ncvsdif  25123  ncvspds  25129  cphnmvs  25158  cphipcl  25159  cphipcj  25167  cphorthcom  25169  cphipval2  25209  4cphipval2  25210  cphipval  25211  fmcfil  25240  mbfi1fseqlem3  25686  mbfi1fseqlem4  25687  mbfi1fseqlem5  25688  deg1ldgdomn  26067  drnguc1p  26147  quotval  26268  sincosq1sgn  26475  sincosq2sgn  26476  sincosq3sgn  26477  sincosq4sgn  26478  efabl  26527  lgsneg1  27301  dchrisumlem3  27470  bdayn0p1  28377  ax5seglem2  29014  usgredg2vtx  29304  uspgredg2vtxeu  29305  usgredg2vtxeu  29306  cplgr3v  29520  vtxdumgr0nedg  29579  clwlkclwwlk  30089  frgrncvvdeqlem8  30393  grpocl  30588  grpodivcl  30627  ablomuldiv  30640  ablodivdiv4  30642  ablonnncan1  30645  vccl  30651  nvgcl  30708  nvcom  30709  nvadd4  30713  nvscl  30714  nvmval  30730  nvmcl  30734  nmcvcn  30783  nmlnoubi  30884  isblo3i  30889  blometi  30891  dipsubdir  30936  hlpar2  30984  hlpar  30985  hlcom  30988  hlipcj  30999  hlipgt0  31002  his52  31175  shintcli  31417  chlub  31597  homulass  31890  adjadj  32024  nmophmi  32119  kbass6  32209  atcvatlem  32473  mdsymlem3  32493  mdsymlem5  32495  suppiniseg  32776  rexdiv  33018  tlt3  33063  toslublem  33065  tosglblem  33067  archiabllem1b  33286  archiabllem2  33291  slmdacl  33303  slmdmcl  33304  slmdvacl  33306  lidlincl  33523  cringm4  33539  evls1fldgencl  33848  aean  34422  fiunelcarsg  34494  probcun  34596  probdif  34598  cndprobin  34612  f1resrcmplf1dlem  35263  rankfilimbi  35278  cusgredgex  35338  swrdwlk  35343  satefvfmla1  35641  climuzcnv  35887  pibt2  37672  matunitlindflem1  37867  mblfinlem1  37908  mblfinlem2  37909  ftc1anclem6  37949  ssbnd  38039  heibor1  38061  exidcl  38127  rngocl  38152  rngogcl  38163  rngocom  38164  rngoa4  38167  rngosub  38181  rngonegmn1l  38192  rngonegmn1r  38193  ispridlc  38321  lshpcmp  39364  opltcon3b  39580  oldmm1  39593  olj01  39601  latm32  39607  omllaw4  39622  omllaw5N  39623  cmtcomlemN  39624  cmt2N  39626  cmtbr2N  39629  cmtbr3N  39630  cmtbr4N  39631  glbconxN  39754  hlexch1  39758  hlexch2  39759  hlexchb1  39760  hlexchb2  39761  hlexch3  39767  hlexch4N  39768  hlatexchb1  39769  hlatexchb2  39770  hlatexch1  39771  hlatexch2  39772  hlatle  39774  hlateq  39775  hlrelat1  39776  hlrelat2  39779  cvr1  39786  cvrval5  39791  cvrp  39792  atcvr1  39793  atcvr2  39794  cvrexchlem  39795  cvrexch  39796  dalem54  40102  pmaple  40137  pmap11  40138  paddass  40214  pmapj2N  40305  pmapocjN  40306  trlval2  40539  nnproddivdvdsd  42370  fsuppssind  42951  mhphf  42955  0prjspnlem  42981  grumnudlem  44641  eelT00  45060  eelTTT  45061  eelT11  45062  eelT12  45064  eelTT1  45065  eelT01  45066  mullimc  45976  mullimcf  45983  dvmptfprod  46303  stoweidlem52  46410  stoweidlem60  46418  focofob  47440  f1ocof1ob  47441  clnbgrgrim  48294  ply1mulgsum  48750  itschlc0xyqsol1  49126  sinhpcosh  50099  reseccl  50112  recsccl  50113  recotcl  50114  onetansqsecsq  50120