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  5617  tz7.5  6332  f1cdmsn  7223  f1ofvswap  7247  f1ofveu  7347  fovcdmda  7524  suppvalfng  8107  smoiso  8292  odi  8504  nndi  8548  nnmsucr  8550  f1oen2g  8901  f1dom2g  8902  domssex2  9061  dif1ennn  9085  enfii  9110  phplem2  9129  php  9131  php3  9133  findcard3  9187  ordunifi  9195  nnsdomg  9204  ackbij1lem16  10147  divneg  11834  divdiv32  11850  divneg2  11866  ltdiv2  12029  fimaxre  12087  fiminre  12090  suprzcl  12574  peano2uz  12820  infssuzle  12850  lbzbi  12855  zbtwnre  12865  irrmul  12893  supxrunb1  13239  expnlbnd  14158  hash1to3  14417  fun2dmnop  14430  brfi1uzind  14433  brcnvtrclfvcnv  14930  retancl  16069  tanneg  16075  demoivreALT  16128  dvdscmulr  16213  dvdsmulcr  16214  mulmoddvds  16259  gcd0id  16448  euclemma  16642  phiprmpw  16705  fermltl  16713  vdwapun  16904  vdwapid1  16905  cshwshashlem1  17025  fsets  17098  pospo  18267  tltnle  18344  latasymb  18366  sgrpcl  18618  mndcl  18634  imasmnd2  18666  gsumsgrpccat  18732  grpcl  18838  dfgrp2  18859  grprcan  18870  grpsubcl  18917  imasgrp2  18952  mhmid  18960  mhmmnd  18961  mulginvcom  18996  mulgnndir  19000  mulgnnass  19006  qusgrp  19083  ghmmulg  19125  ghmrn  19126  ghmeqker  19140  gsumccatsymgsn  19323  ablcom  19696  ablinvadd  19704  mulgmhm  19724  mulgghm  19725  ghmcmn  19728  odadd1  19745  odadd2  19746  rngacl  20065  rngcl  20067  rngpropd  20077  srgcl  20096  srgacl  20108  srgcom  20109  ringcl  20153  crngcom  20154  ringacl  20181  pwspjmhmmgpd  20231  imasring  20233  irredlmul  20331  rhmmul  20389  subrngacl  20459  subrgacl  20486  subrgmcl  20487  subrgugrp  20494  isdomn4  20619  drngmclOLD  20654  isdrngd  20668  isdrngdOLD  20670  srngadd  20754  srngmul  20755  idsrngd  20759  lmodacl  20793  lmodmcl  20794  lmodvacl  20796  lmodvsubcl  20828  lmod4  20833  lmodvaddsub4  20835  lmodvpncan  20836  lmodvnpcan  20837  lmodsubeq0  20842  pwssplit3  20983  islbs2  21079  islbs3  21080  lbsext  21088  rspssp  21164  nzerooringczr  21405  zlmlmod  21447  psgnco  21508  ipdir  21564  ip2eq  21578  ocvin  21599  frlmsplit2  21698  ascldimul  21813  rnasclmulcl  21819  mplbas2  21965  coe1add  22166  coe1subfv  22168  coe1mul2  22171  rhmply1vsca  22291  ringvcl  22303  cramer  22594  chpmat1d  22739  filin  23757  filfinnfr  23780  filuni  23788  ufprim  23812  uffinfix  23830  hausflf  23900  uffcfflf  23942  cnextcn  23970  tmdmulg  23995  tsmsxplem1  24056  psmetcl  24211  xmetcl  24235  metcl  24236  meteq0  24243  metge0  24249  metsym  24254  metgt0  24263  blelrnps  24320  blelrn  24321  blssm  24322  blres  24335  mscl  24365  xmscl  24366  xmsge0  24367  xmseq0  24368  xmssym  24369  mopnin  24401  nmf2  24497  ngpdsr  24509  ngpds2  24510  ngpds2r  24511  ngpds3  24512  ngpds3r  24513  nmge0  24521  nmeq0  24522  nm2dif  24529  nmmul  24568  nlmmul0or  24587  nmods  24648  clmsub  24996  clmacl  25000  clmmcl  25001  clmsubcl  25002  clmvscl  25004  clmvsubval  25025  ncvsprp  25068  ncvsdif  25071  ncvspds  25077  cphnmvs  25106  cphipcl  25107  cphipcj  25115  cphorthcom  25117  cphipval2  25157  4cphipval2  25158  cphipval  25159  fmcfil  25188  mbfi1fseqlem3  25634  mbfi1fseqlem4  25635  mbfi1fseqlem5  25636  deg1ldgdomn  26015  drnguc1p  26095  quotval  26216  sincosq1sgn  26423  sincosq2sgn  26424  sincosq3sgn  26425  sincosq4sgn  26426  efabl  26475  lgsneg1  27249  dchrisumlem3  27418  bdayn0p1  28281  ax5seglem2  28892  usgredg2vtx  29182  uspgredg2vtxeu  29183  usgredg2vtxeu  29184  cplgr3v  29398  vtxdumgr0nedg  29457  clwlkclwwlk  29964  frgrncvvdeqlem8  30268  grpocl  30462  grpodivcl  30501  ablomuldiv  30514  ablodivdiv4  30516  ablonnncan1  30519  vccl  30525  nvgcl  30582  nvcom  30583  nvadd4  30587  nvscl  30588  nvmval  30604  nvmcl  30608  nmcvcn  30657  nmlnoubi  30758  isblo3i  30763  blometi  30765  dipsubdir  30810  hlpar2  30858  hlpar  30859  hlcom  30862  hlipcj  30873  hlipgt0  30876  his52  31049  shintcli  31291  chlub  31471  homulass  31764  adjadj  31898  nmophmi  31993  kbass6  32083  atcvatlem  32347  mdsymlem3  32367  mdsymlem5  32369  suppiniseg  32642  rexdiv  32879  tlt3  32925  toslublem  32927  tosglblem  32929  archiabllem1b  33147  archiabllem2  33152  slmdacl  33164  slmdmcl  33165  slmdvacl  33167  lidlincl  33380  cringm4  33396  evls1fldgencl  33644  aean  34213  fiunelcarsg  34286  probcun  34388  probdif  34390  cndprobin  34404  f1resrcmplf1dlem  35055  cusgredgex  35097  swrdwlk  35102  satefvfmla1  35400  climuzcnv  35646  pibt2  37393  matunitlindflem1  37598  mblfinlem1  37639  mblfinlem2  37640  ftc1anclem6  37680  ssbnd  37770  heibor1  37792  exidcl  37858  rngocl  37883  rngogcl  37894  rngocom  37895  rngoa4  37898  rngosub  37912  rngonegmn1l  37923  rngonegmn1r  37924  ispridlc  38052  lshpcmp  38969  opltcon3b  39185  oldmm1  39198  olj01  39206  latm32  39212  omllaw4  39227  omllaw5N  39228  cmtcomlemN  39229  cmt2N  39231  cmtbr2N  39234  cmtbr3N  39235  cmtbr4N  39236  glbconxN  39360  hlexch1  39364  hlexch2  39365  hlexchb1  39366  hlexchb2  39367  hlexch3  39373  hlexch4N  39374  hlatexchb1  39375  hlatexchb2  39376  hlatexch1  39377  hlatexch2  39378  hlatle  39380  hlateq  39381  hlrelat1  39382  hlrelat2  39385  cvr1  39392  cvrval5  39397  cvrp  39398  atcvr1  39399  atcvr2  39400  cvrexchlem  39401  cvrexch  39402  dalem54  39708  pmaple  39743  pmap11  39744  paddass  39820  pmapj2N  39911  pmapocjN  39912  trlval2  40145  nnproddivdvdsd  41976  fsuppssind  42569  mhphf  42573  0prjspnlem  42599  grumnudlem  44261  eelT00  44681  eelTTT  44682  eelT11  44683  eelT12  44685  eelTT1  44686  eelT01  44687  mullimc  45601  mullimcf  45608  dvmptfprod  45930  stoweidlem52  46037  stoweidlem60  46045  focofob  47068  f1ocof1ob  47069  clnbgrgrim  47922  ply1mulgsum  48379  itschlc0xyqsol1  48755  sinhpcosh  49729  reseccl  49742  recsccl  49743  recotcl  49744  onetansqsecsq  49750