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  5613  tz7.5  6333  f1cdmsn  7222  f1ofvswap  7246  f1ofveu  7346  fovcdmda  7523  suppvalfng  8103  smoiso  8288  odi  8500  nndi  8544  nnmsucr  8546  f1oen2g  8897  f1dom2g  8898  domssex2  9056  dif1ennn  9078  enfii  9101  phplem2  9120  php  9122  php3  9124  findcard3  9173  ordunifi  9180  nnsdomg  9189  ackbij1lem16  10131  divneg  11819  divdiv32  11835  divneg2  11851  ltdiv2  12014  fimaxre  12072  fiminre  12075  suprzcl  12559  peano2uz  12805  infssuzle  12835  lbzbi  12840  zbtwnre  12850  irrmul  12878  supxrunb1  13224  expnlbnd  14146  hash1to3  14405  fun2dmnop  14418  brfi1uzind  14421  brcnvtrclfvcnv  14918  retancl  16057  tanneg  16063  demoivreALT  16116  dvdscmulr  16201  dvdsmulcr  16202  mulmoddvds  16247  gcd0id  16436  euclemma  16630  phiprmpw  16693  fermltl  16701  vdwapun  16892  vdwapid1  16893  cshwshashlem1  17013  fsets  17086  pospo  18255  tltnle  18332  latasymb  18354  sgrpcl  18640  mndcl  18656  imasmnd2  18688  gsumsgrpccat  18754  grpcl  18860  dfgrp2  18881  grprcan  18892  grpsubcl  18939  imasgrp2  18974  mhmid  18982  mhmmnd  18983  mulginvcom  19018  mulgnndir  19022  mulgnnass  19028  qusgrp  19104  ghmmulg  19146  ghmrn  19147  ghmeqker  19161  gsumccatsymgsn  19344  ablcom  19717  ablinvadd  19725  mulgmhm  19745  mulgghm  19746  ghmcmn  19749  odadd1  19766  odadd2  19767  rngacl  20086  rngcl  20088  rngpropd  20098  srgcl  20117  srgacl  20129  srgcom  20130  ringcl  20174  crngcom  20175  ringacl  20202  pwspjmhmmgpd  20252  imasring  20254  irredlmul  20352  rhmmul  20409  subrngacl  20477  subrgacl  20504  subrgmcl  20505  subrgugrp  20512  isdomn4  20637  drngmclOLD  20672  isdrngd  20686  isdrngdOLD  20688  srngadd  20772  srngmul  20773  idsrngd  20777  lmodacl  20811  lmodmcl  20812  lmodvacl  20814  lmodvsubcl  20846  lmod4  20851  lmodvaddsub4  20853  lmodvpncan  20854  lmodvnpcan  20855  lmodsubeq0  20860  pwssplit3  21001  islbs2  21097  islbs3  21098  lbsext  21106  rspssp  21182  nzerooringczr  21423  zlmlmod  21465  psgnco  21526  ipdir  21582  ip2eq  21596  ocvin  21617  frlmsplit2  21716  ascldimul  21831  rnasclmulcl  21837  mplbas2  21983  coe1add  22184  coe1subfv  22186  coe1mul2  22189  rhmply1vsca  22309  ringvcl  22321  cramer  22612  chpmat1d  22757  filin  23775  filfinnfr  23798  filuni  23806  ufprim  23830  uffinfix  23848  hausflf  23918  uffcfflf  23960  cnextcn  23988  tmdmulg  24013  tsmsxplem1  24074  psmetcl  24228  xmetcl  24252  metcl  24253  meteq0  24260  metge0  24266  metsym  24271  metgt0  24280  blelrnps  24337  blelrn  24338  blssm  24339  blres  24352  mscl  24382  xmscl  24383  xmsge0  24384  xmseq0  24385  xmssym  24386  mopnin  24418  nmf2  24514  ngpdsr  24526  ngpds2  24527  ngpds2r  24528  ngpds3  24529  ngpds3r  24530  nmge0  24538  nmeq0  24539  nm2dif  24546  nmmul  24585  nlmmul0or  24604  nmods  24665  clmsub  25013  clmacl  25017  clmmcl  25018  clmsubcl  25019  clmvscl  25021  clmvsubval  25042  ncvsprp  25085  ncvsdif  25088  ncvspds  25094  cphnmvs  25123  cphipcl  25124  cphipcj  25132  cphorthcom  25134  cphipval2  25174  4cphipval2  25175  cphipval  25176  fmcfil  25205  mbfi1fseqlem3  25651  mbfi1fseqlem4  25652  mbfi1fseqlem5  25653  deg1ldgdomn  26032  drnguc1p  26112  quotval  26233  sincosq1sgn  26440  sincosq2sgn  26441  sincosq3sgn  26442  sincosq4sgn  26443  efabl  26492  lgsneg1  27266  dchrisumlem3  27435  bdayn0p1  28300  ax5seglem2  28914  usgredg2vtx  29204  uspgredg2vtxeu  29205  usgredg2vtxeu  29206  cplgr3v  29420  vtxdumgr0nedg  29479  clwlkclwwlk  29989  frgrncvvdeqlem8  30293  grpocl  30487  grpodivcl  30526  ablomuldiv  30539  ablodivdiv4  30541  ablonnncan1  30544  vccl  30550  nvgcl  30607  nvcom  30608  nvadd4  30612  nvscl  30613  nvmval  30629  nvmcl  30633  nmcvcn  30682  nmlnoubi  30783  isblo3i  30788  blometi  30790  dipsubdir  30835  hlpar2  30883  hlpar  30884  hlcom  30887  hlipcj  30898  hlipgt0  30901  his52  31074  shintcli  31316  chlub  31496  homulass  31789  adjadj  31923  nmophmi  32018  kbass6  32108  atcvatlem  32372  mdsymlem3  32392  mdsymlem5  32394  suppiniseg  32674  rexdiv  32913  tlt3  32958  toslublem  32960  tosglblem  32962  archiabllem1b  33168  archiabllem2  33173  slmdacl  33185  slmdmcl  33186  slmdvacl  33188  lidlincl  33402  cringm4  33418  evls1fldgencl  33690  aean  34264  fiunelcarsg  34336  probcun  34438  probdif  34440  cndprobin  34454  f1resrcmplf1dlem  35105  rankfilimbi  35119  cusgredgex  35173  swrdwlk  35178  satefvfmla1  35476  climuzcnv  35722  pibt2  37468  matunitlindflem1  37662  mblfinlem1  37703  mblfinlem2  37704  ftc1anclem6  37744  ssbnd  37834  heibor1  37856  exidcl  37922  rngocl  37947  rngogcl  37958  rngocom  37959  rngoa4  37962  rngosub  37976  rngonegmn1l  37987  rngonegmn1r  37988  ispridlc  38116  lshpcmp  39093  opltcon3b  39309  oldmm1  39322  olj01  39330  latm32  39336  omllaw4  39351  omllaw5N  39352  cmtcomlemN  39353  cmt2N  39355  cmtbr2N  39358  cmtbr3N  39359  cmtbr4N  39360  glbconxN  39483  hlexch1  39487  hlexch2  39488  hlexchb1  39489  hlexchb2  39490  hlexch3  39496  hlexch4N  39497  hlatexchb1  39498  hlatexchb2  39499  hlatexch1  39500  hlatexch2  39501  hlatle  39503  hlateq  39504  hlrelat1  39505  hlrelat2  39508  cvr1  39515  cvrval5  39520  cvrp  39521  atcvr1  39522  atcvr2  39523  cvrexchlem  39524  cvrexch  39525  dalem54  39831  pmaple  39866  pmap11  39867  paddass  39943  pmapj2N  40034  pmapocjN  40035  trlval2  40268  nnproddivdvdsd  42099  fsuppssind  42692  mhphf  42696  0prjspnlem  42722  grumnudlem  44383  eelT00  44802  eelTTT  44803  eelT11  44804  eelT12  44806  eelTT1  44807  eelT01  44808  mullimc  45721  mullimcf  45728  dvmptfprod  46048  stoweidlem52  46155  stoweidlem60  46163  focofob  47185  f1ocof1ob  47186  clnbgrgrim  48039  ply1mulgsum  48496  itschlc0xyqsol1  48872  sinhpcosh  49846  reseccl  49859  recsccl  49860  recotcl  49861  onetansqsecsq  49867