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 207  df-an 396  df-3an 1089

This theorem is referenced by:  3adant1l  1176  3adant1r  1177  syl3an1b  1403  syl3an1br  1406  wefrc  5694  tz7.5  6416  f1cdmsn  7318  f1ofvswap  7342  f1ofveu  7442  fovcdmda  7621  suppvalfng  8208  smoiso  8418  odi  8635  nndi  8679  nnmsucr  8681  f1oen2g  9028  f1dom2g  9029  f1dom2gOLD  9030  domssex2  9203  dif1ennn  9227  enfii  9252  phplem2  9271  php  9273  php3  9275  findcard3  9346  ordunifi  9354  nnsdomg  9363  ackbij1lem16  10303  divneg  11986  divdiv32  12002  divneg2  12018  ltdiv2  12181  fimaxre  12239  fiminre  12242  suprzcl  12723  peano2uz  12966  infssuzle  12996  lbzbi  13001  zbtwnre  13011  irrmul  13039  supxrunb1  13381  expnlbnd  14282  hash1to3  14541  fun2dmnop  14554  brfi1uzind  14557  brcnvtrclfvcnv  15054  retancl  16190  tanneg  16196  demoivreALT  16249  dvdscmulr  16333  dvdsmulcr  16334  mulmoddvds  16378  gcd0id  16565  euclemma  16760  phiprmpw  16823  fermltl  16831  vdwapun  17021  vdwapid1  17022  cshwshashlem1  17143  fsets  17216  pospo  18415  tltnle  18492  latasymb  18512  sgrpcl  18764  mndcl  18780  imasmnd2  18809  gsumsgrpccat  18875  grpcl  18981  dfgrp2  19002  grprcan  19013  grpsubcl  19060  imasgrp2  19095  mhmid  19103  mhmmnd  19104  mulginvcom  19139  mulgnndir  19143  mulgnnass  19149  qusgrp  19226  ghmmulg  19268  ghmrn  19269  ghmeqker  19283  gsumccatsymgsn  19468  ablcom  19841  ablinvadd  19849  mulgmhm  19869  mulgghm  19870  ghmcmn  19873  odadd1  19890  odadd2  19891  rngacl  20189  rngcl  20191  rngpropd  20201  srgcl  20220  srgacl  20232  srgcom  20233  ringcl  20277  crngcom  20278  ringacl  20301  pwspjmhmmgpd  20351  imasring  20353  irredlmul  20454  rhmmul  20512  subrngacl  20582  subrgacl  20611  subrgmcl  20612  subrgugrp  20619  isdomn4  20738  drngmclOLD  20773  isdrngd  20787  isdrngdOLD  20789  srngadd  20874  srngmul  20875  idsrngd  20879  lmodacl  20892  lmodmcl  20893  lmodvacl  20895  lmodvsubcl  20927  lmod4  20932  lmodvaddsub4  20934  lmodvpncan  20935  lmodvnpcan  20936  lmodsubeq0  20941  pwssplit3  21083  islbs2  21179  islbs3  21180  lbsext  21188  rspssp  21272  nzerooringczr  21514  zlmlmod  21560  psgnco  21624  ipdir  21680  ip2eq  21694  ocvin  21715  frlmsplit2  21816  ascldimul  21931  rnasclmulcl  21937  mplbas2  22083  coe1add  22288  coe1subfv  22290  coe1mul2  22293  rhmply1vsca  22413  ringvcl  22425  cramer  22718  chpmat1d  22863  filin  23883  filfinnfr  23906  filuni  23914  ufprim  23938  uffinfix  23956  hausflf  24026  uffcfflf  24068  cnextcn  24096  tmdmulg  24121  tsmsxplem1  24182  psmetcl  24338  xmetcl  24362  metcl  24363  meteq0  24370  metge0  24376  metsym  24381  metgt0  24390  blelrnps  24447  blelrn  24448  blssm  24449  blres  24462  mscl  24492  xmscl  24493  xmsge0  24494  xmseq0  24495  xmssym  24496  mopnin  24531  nmf2  24627  ngpdsr  24639  ngpds2  24640  ngpds2r  24641  ngpds3  24642  ngpds3r  24643  nmge0  24651  nmeq0  24652  nm2dif  24659  nmmul  24706  nlmmul0or  24725  nmods  24786  clmsub  25132  clmacl  25136  clmmcl  25137  clmsubcl  25138  clmvscl  25140  clmvsubval  25161  ncvsprp  25205  ncvsdif  25208  ncvspds  25214  cphnmvs  25243  cphipcl  25244  cphipcj  25252  cphorthcom  25254  cphipval2  25294  4cphipval2  25295  cphipval  25296  fmcfil  25325  mbfi1fseqlem3  25772  mbfi1fseqlem4  25773  mbfi1fseqlem5  25774  deg1ldgdomn  26153  drnguc1p  26233  quotval  26352  sincosq1sgn  26558  sincosq2sgn  26559  sincosq3sgn  26560  sincosq4sgn  26561  efabl  26610  lgsneg1  27384  dchrisumlem3  27553  ax5seglem2  28962  usgredg2vtx  29254  uspgredg2vtxeu  29255  usgredg2vtxeu  29256  cplgr3v  29470  vtxdumgr0nedg  29529  clwlkclwwlk  30034  frgrncvvdeqlem8  30338  grpocl  30532  grpodivcl  30571  ablomuldiv  30584  ablodivdiv4  30586  ablonnncan1  30589  vccl  30595  nvgcl  30652  nvcom  30653  nvadd4  30657  nvscl  30658  nvmval  30674  nvmcl  30678  nmcvcn  30727  nmlnoubi  30828  isblo3i  30833  blometi  30835  dipsubdir  30880  hlpar2  30928  hlpar  30929  hlcom  30932  hlipcj  30943  hlipgt0  30946  his52  31119  shintcli  31361  chlub  31541  homulass  31834  adjadj  31968  nmophmi  32063  kbass6  32153  atcvatlem  32417  mdsymlem3  32437  mdsymlem5  32439  suppiniseg  32698  rexdiv  32890  tlt3  32943  toslublem  32945  tosglblem  32947  archiabllem1b  33172  archiabllem2  33177  slmdacl  33188  slmdmcl  33189  slmdvacl  33191  lidlincl  33423  cringm4  33439  evls1fldgencl  33680  aean  34208  fiunelcarsg  34281  probcun  34383  probdif  34385  cndprobin  34399  f1resrcmplf1dlem  35062  cusgredgex  35089  swrdwlk  35094  satefvfmla1  35393  climuzcnv  35639  pibt2  37383  matunitlindflem1  37576  mblfinlem1  37617  mblfinlem2  37618  ftc1anclem6  37658  ssbnd  37748  heibor1  37770  exidcl  37836  rngocl  37861  rngogcl  37872  rngocom  37873  rngoa4  37876  rngosub  37890  rngonegmn1l  37901  rngonegmn1r  37902  ispridlc  38030  lshpcmp  38944  opltcon3b  39160  oldmm1  39173  olj01  39181  latm32  39187  omllaw4  39202  omllaw5N  39203  cmtcomlemN  39204  cmt2N  39206  cmtbr2N  39209  cmtbr3N  39210  cmtbr4N  39211  glbconxN  39335  hlexch1  39339  hlexch2  39340  hlexchb1  39341  hlexchb2  39342  hlexch3  39348  hlexch4N  39349  hlatexchb1  39350  hlatexchb2  39351  hlatexch1  39352  hlatexch2  39353  hlatle  39355  hlateq  39356  hlrelat1  39357  hlrelat2  39360  cvr1  39367  cvrval5  39372  cvrp  39373  atcvr1  39374  atcvr2  39375  cvrexchlem  39376  cvrexch  39377  dalem54  39683  pmaple  39718  pmap11  39719  paddass  39795  pmapj2N  39886  pmapocjN  39887  trlval2  40120  nnproddivdvdsd  41957  fsuppssind  42548  mhphf  42552  0prjspnlem  42578  grumnudlem  44254  eelT00  44676  eelTTT  44677  eelT11  44678  eelT12  44680  eelTT1  44681  eelT01  44682  mullimc  45537  mullimcf  45544  stoweidlem52  45973  stoweidlem60  45981  focofob  46995  f1ocof1ob  46996  clnbgrgrim  47786  ply1mulgsum  48119  itschlc0xyqsol1  48500  sinhpcosh  48832  reseccl  48845  recsccl  48846  recotcl  48847  onetansqsecsq  48853