MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl3an1 Structured version   Visualization version   GIF version

Theorem syl3an1 1166
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
StepHypRef Expression
1 syl3an1.1 . . 3 (𝜑𝜓)
213anim1i 1155 . 2 ((𝜑𝜒𝜃) → (𝜓𝜒𝜃))
3 syl3an1.2 . 2 ((𝜓𝜒𝜃) → 𝜏)
42, 3syl 17 1 ((𝜑𝜒𝜃) → 𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1071
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 197  df-an 383  df-3an 1073
This theorem is referenced by:  3adant1l  1185  3adant1r  1187  syl3an1b  1509  syl3an1br  1512  wefrc  5243  tz7.5  5887  f1ofveu  6788  fovrnda  6952  smoiso  7612  odi  7813  nndi  7857  nnmsucr  7859  f1oen2g  8126  f1dom2g  8127  domssex2  8276  ordunifi  8366  wemappo  8610  wemapso  8612  ackbij1lem16  9259  divneg  10921  divdiv32  10935  divneg2  10951  ltdiv2  11111  fimaxre  11170  suprzcl  11659  peano2uz  11943  infssuzle  11974  lbzbi  11979  zbtwnre  11989  irrmul  12016  supxrunb1  12354  expnlbnd  13201  hash1to3  13475  fun2dmnop  13479  brfi1uzind  13482  brcnvtrclfvcnv  13954  retancl  15078  tanneg  15084  demoivreALT  15137  dvdscmulr  15219  dvdsmulcr  15220  mulmoddvds  15260  gcd0id  15448  euclemma  15632  phiprmpw  15688  fermltl  15696  vdwapun  15885  vdwapid1  15886  cshwshashlem1  16009  fsets  16098  pospo  17181  latasymb  17262  mndcl  17509  imasmnd2  17535  grpcl  17638  dfgrp2  17655  grprcan  17663  grpsubcl  17703  imasgrp2  17738  mhmid  17744  mhmmnd  17745  mulginvcom  17773  qusgrp  17857  ghmmulg  17880  ghmrn  17881  ghmeqker  17895  gsumccatsymgsn  18053  ablcom  18417  ablinvadd  18422  mulgmhm  18440  mulgghm  18441  ghmcmn  18444  odadd1  18458  odadd2  18459  srgcl  18720  srgacl  18732  srgcom  18733  ringcl  18769  crngcom  18770  ringacl  18786  imasring  18827  irredlmul  18916  rhmmul  18937  drngmcl  18970  isdrngd  18982  subrgacl  19001  subrgugrp  19009  srngadd  19067  srngmul  19068  idsrngd  19072  lmodacl  19084  lmodmcl  19085  lmodvacl  19087  lmodvsubcl  19118  lmod4  19123  lmodvaddsub4  19125  lmodvpncan  19126  lmodvnpcan  19127  lmodsubeq0  19132  pwssplit3  19274  islbs2  19369  islbs3  19370  lbsext  19378  rspssp  19441  mplbas2  19685  coe1add  19849  coe1subfv  19851  coe1mul2  19854  zlmlmod  20086  psgnco  20144  ipdir  20201  ip2eq  20215  ocvin  20235  frlmsplit2  20329  ringvcl  20421  cramer  20717  chpmat1d  20861  filin  21878  filfinnfr  21901  filuni  21909  ufprim  21933  uffinfix  21951  hausflf  22021  uffcfflf  22063  cnextcn  22091  tmdmulg  22116  tsmsxplem1  22176  psmetcl  22332  xmetcl  22356  metcl  22357  meteq0  22364  metge0  22370  metsym  22375  metgt0  22384  blelrnps  22441  blelrn  22442  blssm  22443  blres  22456  mscl  22486  xmscl  22487  xmsge0  22488  xmseq0  22489  xmssym  22490  mopnin  22522  nmf2  22617  ngpdsr  22629  ngpds2  22630  ngpds2r  22631  ngpds3  22632  ngpds3r  22633  nmge0  22641  nmeq0  22642  nm2dif  22649  nmmul  22688  nlmmul0or  22707  nmods  22768  clmsub  23099  clmacl  23103  clmmcl  23104  clmsubcl  23105  clmvscl  23107  clmvsubval  23128  ncvsprp  23171  ncvsdif  23174  ncvspds  23180  cphnmvs  23209  cphipcl  23210  cphipcj  23218  cphorthcom  23220  cphipval2  23259  4cphipval2  23260  cphipval  23261  fmcfil  23289  mbfi1fseqlem3  23704  mbfi1fseqlem4  23705  mbfi1fseqlem5  23706  deg1ldgdomn  24074  drnguc1p  24150  quotval  24267  sincosq1sgn  24471  sincosq2sgn  24472  sincosq3sgn  24473  sincosq4sgn  24474  efabl  24517  lgsneg1  25268  dchrisumlem3  25401  ax5seglem2  26030  usgredg2vtx  26333  uspgredg2vtxeu  26334  usgredg2vtxeu  26335  cplgr3v  26566  vtxdumgr0nedg  26624  wlkwwlkinjOLD  27031  wlkwwlksurOLD  27032  clwlkclwwlk  27152  clwlksfclwwlkOLD  27243  frgrncvvdeqlem8  27488  grpocl  27694  grpodivcl  27733  ablomuldiv  27746  ablodivdiv4  27748  ablonnncan  27750  ablonnncan1  27752  vccl  27758  nvgcl  27815  nvcom  27816  nvadd4  27820  nvscl  27821  nvmval  27837  nvmcl  27841  nmcvcn  27890  nmlnoubi  27991  isblo3i  27996  blometi  27998  dipsubdir  28043  hlpar2  28092  hlpar  28093  hlcom  28096  hlipcj  28107  hlipgt0  28110  his52  28284  shintcli  28528  chlub  28708  homulass  29001  adjadj  29135  nmophmi  29230  kbass6  29320  atcvatlem  29584  mdsymlem3  29604  mdsymlem5  29606  rexdiv  29974  tltnle  30002  tlt3  30005  toslublem  30007  tosglblem  30009  archiabllem1b  30086  archiabllem2  30091  slmdacl  30102  slmdmcl  30103  slmdvacl  30105  aean  30647  fiunelcarsg  30718  probcun  30820  probdif  30822  cndprobin  30836  climuzcnv  31903  matunitlindflem1  33738  mblfinlem1  33779  mblfinlem2  33780  ftc1anclem6  33822  ssbnd  33919  heibor1  33941  exidcl  34007  rngocl  34032  rngogcl  34043  rngocom  34044  rngoa4  34047  rngosub  34061  rngonegmn1l  34072  rngonegmn1r  34073  ispridlc  34201  lshpcmp  34797  opltcon3b  35013  oldmm1  35026  olj01  35034  latm32  35040  omllaw4  35055  omllaw5N  35056  cmtcomlemN  35057  cmt2N  35059  cmtbr2N  35062  cmtbr3N  35063  cmtbr4N  35064  glbconxN  35186  hlexch1  35190  hlexch2  35191  hlexchb1  35192  hlexchb2  35193  hlexch3  35199  hlexch4N  35200  hlatexchb1  35201  hlatexchb2  35202  hlatexch1  35203  hlatexch2  35204  hlatle  35206  hlateq  35207  hlrelat1  35208  hlrelat2  35211  cvr1  35218  cvrval5  35223  cvrp  35224  atcvr1  35225  atcvr2  35226  cvrexchlem  35227  cvrexch  35228  dalem54  35534  pmaple  35569  pmap11  35570  paddass  35646  pmapj2N  35737  pmapocjN  35738  trlval2  35972  eelT00  39455  eelTTT  39456  eelT11  39457  eelT12  39459  eelTT1  39460  eelT01  39461  mullimc  40366  mullimcf  40373  stoweidlem52  40786  stoweidlem60  40794  rngcl  42411  nzerooringczr  42600  ply1mulgsum  42706  sinhpcosh  43012  reseccl  43025  recsccl  43026  recotcl  43027  onetansqsecsq  43033
  Copyright terms: Public domain W3C validator