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 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 206  df-an 397  df-3an 1089

This theorem is referenced by:  3adant1l  1176  3adant1r  1177  syl3an1b  1403  syl3an1br  1406  wefrc  5669  tz7.5  6382  f1cdmsn  7276  f1ofvswap  7300  f1ofveu  7399  fovcdmda  7574  suppvalfng  8149  smoiso  8358  odi  8575  nndi  8619  nnmsucr  8621  f1oen2g  8960  f1dom2g  8961  f1dom2gOLD  8962  domssex2  9133  dif1ennn  9157  enfii  9185  phplem2  9204  php  9206  php3  9208  findcard3  9281  ordunifi  9289  nnsdomg  9298  ackbij1lem16  10226  divneg  11902  divdiv32  11918  divneg2  11934  ltdiv2  12096  fimaxre  12154  fiminre  12157  suprzcl  12638  peano2uz  12881  infssuzle  12911  lbzbi  12916  zbtwnre  12926  irrmul  12954  supxrunb1  13294  expnlbnd  14192  hash1to3  14448  fun2dmnop  14452  brfi1uzind  14455  brcnvtrclfvcnv  14948  retancl  16081  tanneg  16087  demoivreALT  16140  dvdscmulr  16224  dvdsmulcr  16225  mulmoddvds  16269  gcd0id  16456  euclemma  16646  phiprmpw  16705  fermltl  16713  vdwapun  16903  vdwapid1  16904  cshwshashlem1  17025  fsets  17098  pospo  18294  tltnle  18371  latasymb  18391  sgrpcl  18613  mndcl  18629  imasmnd2  18658  gsumsgrpccat  18717  grpcl  18823  dfgrp2  18843  grprcan  18854  grpsubcl  18899  imasgrp2  18934  mhmid  18940  mhmmnd  18941  mulginvcom  18973  mulgnndir  18977  mulgnnass  18983  qusgrp  19059  ghmmulg  19098  ghmrn  19099  ghmeqker  19113  gsumccatsymgsn  19288  ablcom  19661  ablinvadd  19669  mulgmhm  19689  mulgghm  19690  ghmcmn  19693  odadd1  19710  odadd2  19711  srgcl  20009  srgacl  20021  srgcom  20022  ringcl  20066  crngcom  20067  ringacl  20088  pwspjmhmmgpd  20134  imasring  20136  irredlmul  20234  rhmmul  20256  drngmcl  20324  isdrngd  20340  isdrngdOLD  20342  subrgacl  20366  subrgugrp  20374  srngadd  20457  srngmul  20458  idsrngd  20462  lmodacl  20475  lmodmcl  20476  lmodvacl  20478  lmodvsubcl  20509  lmod4  20514  lmodvaddsub4  20516  lmodvpncan  20517  lmodvnpcan  20518  lmodsubeq0  20523  pwssplit3  20664  islbs2  20759  islbs3  20760  lbsext  20768  rspssp  20843  isdomn4  20910  zlmlmod  21067  psgnco  21127  ipdir  21183  ip2eq  21197  ocvin  21218  frlmsplit2  21319  ascldimul  21433  rnasclmulcl  21439  mplbas2  21588  coe1add  21777  coe1subfv  21779  coe1mul2  21782  ringvcl  21891  cramer  22184  chpmat1d  22329  filin  23349  filfinnfr  23372  filuni  23380  ufprim  23404  uffinfix  23422  hausflf  23492  uffcfflf  23534  cnextcn  23562  tmdmulg  23587  tsmsxplem1  23648  psmetcl  23804  xmetcl  23828  metcl  23829  meteq0  23836  metge0  23842  metsym  23847  metgt0  23856  blelrnps  23913  blelrn  23914  blssm  23915  blres  23928  mscl  23958  xmscl  23959  xmsge0  23960  xmseq0  23961  xmssym  23962  mopnin  23997  nmf2  24093  ngpdsr  24105  ngpds2  24106  ngpds2r  24107  ngpds3  24108  ngpds3r  24109  nmge0  24117  nmeq0  24118  nm2dif  24125  nmmul  24172  nlmmul0or  24191  nmods  24252  clmsub  24587  clmacl  24591  clmmcl  24592  clmsubcl  24593  clmvscl  24595  clmvsubval  24616  ncvsprp  24660  ncvsdif  24663  ncvspds  24669  cphnmvs  24698  cphipcl  24699  cphipcj  24707  cphorthcom  24709  cphipval2  24749  4cphipval2  24750  cphipval  24751  fmcfil  24780  mbfi1fseqlem3  25226  mbfi1fseqlem4  25227  mbfi1fseqlem5  25228  deg1ldgdomn  25603  drnguc1p  25679  quotval  25796  sincosq1sgn  25999  sincosq2sgn  26000  sincosq3sgn  26001  sincosq4sgn  26002  efabl  26050  lgsneg1  26814  dchrisumlem3  26983  ax5seglem2  28176  usgredg2vtx  28465  uspgredg2vtxeu  28466  usgredg2vtxeu  28467  cplgr3v  28681  vtxdumgr0nedg  28739  clwlkclwwlk  29244  frgrncvvdeqlem8  29548  grpocl  29740  grpodivcl  29779  ablomuldiv  29792  ablodivdiv4  29794  ablonnncan1  29797  vccl  29803  nvgcl  29860  nvcom  29861  nvadd4  29865  nvscl  29866  nvmval  29882  nvmcl  29886  nmcvcn  29935  nmlnoubi  30036  isblo3i  30041  blometi  30043  dipsubdir  30088  hlpar2  30136  hlpar  30137  hlcom  30140  hlipcj  30151  hlipgt0  30154  his52  30327  shintcli  30569  chlub  30749  homulass  31042  adjadj  31176  nmophmi  31271  kbass6  31361  atcvatlem  31625  mdsymlem3  31645  mdsymlem5  31647  suppiniseg  31895  rexdiv  32079  tlt3  32127  toslublem  32129  tosglblem  32131  archiabllem1b  32325  archiabllem2  32330  slmdacl  32341  slmdmcl  32342  slmdvacl  32344  lidlincl  32536  cringm4  32553  aean  33230  fiunelcarsg  33303  probcun  33405  probdif  33407  cndprobin  33421  f1resrcmplf1dlem  34077  cusgredgex  34100  swrdwlk  34105  satefvfmla1  34404  climuzcnv  34644  pibt2  36286  matunitlindflem1  36472  mblfinlem1  36513  mblfinlem2  36514  ftc1anclem6  36554  ssbnd  36644  heibor1  36666  exidcl  36732  rngocl  36757  rngogcl  36768  rngocom  36769  rngoa4  36772  rngosub  36786  rngonegmn1l  36797  rngonegmn1r  36798  ispridlc  36926  lshpcmp  37846  opltcon3b  38062  oldmm1  38075  olj01  38083  latm32  38089  omllaw4  38104  omllaw5N  38105  cmtcomlemN  38106  cmt2N  38108  cmtbr2N  38111  cmtbr3N  38112  cmtbr4N  38113  glbconxN  38237  hlexch1  38241  hlexch2  38242  hlexchb1  38243  hlexchb2  38244  hlexch3  38250  hlexch4N  38251  hlatexchb1  38252  hlatexchb2  38253  hlatexch1  38254  hlatexch2  38255  hlatle  38257  hlateq  38258  hlrelat1  38259  hlrelat2  38262  cvr1  38269  cvrval5  38274  cvrp  38275  atcvr1  38276  atcvr2  38277  cvrexchlem  38278  cvrexch  38279  dalem54  38585  pmaple  38620  pmap11  38621  paddass  38697  pmapj2N  38788  pmapocjN  38789  trlval2  39022  nnproddivdvdsd  40854  fsuppssind  41162  mhphf  41166  0prjspnlem  41361  grumnudlem  43029  eelT00  43451  eelTTT  43452  eelT11  43453  eelT12  43455  eelTT1  43456  eelT01  43457  mullimc  44318  mullimcf  44325  stoweidlem52  44754  stoweidlem60  44762  focofob  45774  f1ocof1ob  45775  rngacl  46647  rngcl  46649  rngpropd  46659  subrngacl  46719  nzerooringczr  46923  ply1mulgsum  47024  itschlc0xyqsol1  47405  sinhpcosh  47738  reseccl  47751  recsccl  47752  recotcl  47753  onetansqsecsq  47759