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

Theorem syl3an1 1356
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 1246 . 2 ((𝜑𝜒𝜃) → (𝜓𝜒𝜃))
3 syl3an1.2 . 2 ((𝜓𝜒𝜃) → 𝜏)
42, 3syl 17 1 ((𝜑𝜒𝜃) → 𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1036
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 386  df-3an 1038
This theorem is referenced by:  syl3an1b  1359  syl3an1br  1362  wefrc  5073  tz7.5  5708  f1ofveu  6605  fovrnda  6765  smoiso  7411  odi  7611  nndi  7655  nnmsucr  7657  f1oen2g  7924  f1dom2g  7925  domssex2  8072  ordunifi  8162  wemappo  8406  wemapso  8408  ackbij1lem16  9009  divneg  10671  divdiv32  10685  divneg2  10701  ltdiv2  10861  fimaxre  10920  suprzcl  11409  peano2uz  11693  infssuzle  11723  lbzbi  11728  zbtwnre  11738  irrmul  11765  supxrunb1  12100  expnlbnd  12942  hash1to3  13220  fun2dmnop  13224  brfi1uzind  13227  brfi1uzindOLD  13233  brcnvtrclfvcnv  13688  retancl  14808  tanneg  14814  demoivreALT  14867  dvdscmulr  14945  dvdsmulcr  14946  gcd0id  15175  euclemma  15360  phiprmpw  15416  fermltl  15424  vdwapun  15613  vdwapid1  15614  cshwshashlem1  15737  fsets  15823  pospo  16905  latasymb  16986  mndcl  17233  imasmnd2  17259  grpcl  17362  dfgrp2  17379  grprcan  17387  grpsubcl  17427  imasgrp2  17462  mhmid  17468  mhmmnd  17469  mulginvcom  17497  qusgrp  17581  ghmmulg  17604  ghmrn  17605  ghmeqker  17619  gsumccatsymgsn  17778  ablcom  18142  ablinvadd  18147  mulgmhm  18165  mulgghm  18166  ghmcmn  18169  odadd1  18183  odadd2  18184  srgcl  18444  srgacl  18456  srgcom  18457  ringcl  18493  crngcom  18494  ringacl  18510  imasring  18551  irredlmul  18640  rhmmul  18659  drngmcl  18692  isdrngd  18704  subrgacl  18723  subrgugrp  18731  srngadd  18789  srngmul  18790  idsrngd  18794  lmodacl  18806  lmodmcl  18807  lmodvacl  18809  lmodvsubcl  18840  lmod4  18845  lmodvaddsub4  18847  lmodvpncan  18848  lmodvnpcan  18849  lmodsubeq0  18854  pwssplit3  18993  islbs2  19086  islbs3  19087  lbsext  19095  rspssp  19158  mplbas2  19402  coe1add  19566  coe1subfv  19568  coe1mul2  19571  zlmlmod  19803  psgnco  19861  ipdir  19916  ip2eq  19930  ocvin  19950  frlmsplit2  20044  ringvcl  20136  cramer  20429  chpmat1d  20573  filin  21581  filfinnfr  21604  filuni  21612  ufprim  21636  uffinfix  21654  hausflf  21724  uffcfflf  21766  cnextcn  21794  tmdmulg  21819  tsmsxplem1  21879  psmetcl  22035  xmetcl  22059  metcl  22060  meteq0  22067  metge0  22073  metsym  22078  metgt0  22087  blelrnps  22144  blelrn  22145  blssm  22146  blres  22159  mscl  22189  xmscl  22190  xmsge0  22191  xmseq0  22192  xmssym  22193  mopnin  22225  nmf2  22320  ngpdsr  22332  ngpds2  22333  ngpds2r  22334  ngpds3  22335  ngpds3r  22336  nmge0  22344  nmeq0  22345  nm2dif  22352  nmmul  22391  nlmmul0or  22410  nmods  22471  clmsub  22803  clmacl  22807  clmmcl  22808  clmsubcl  22809  clmvscl  22811  clmvsubval  22832  ncvsprp  22875  ncvsdif  22878  ncvspds  22884  cphnmvs  22913  cphipcl  22914  cphipcj  22922  cphorthcom  22924  cphipval2  22963  4cphipval2  22964  cphipval  22965  fmcfil  22993  mbfi1fseqlem3  23407  mbfi1fseqlem4  23408  mbfi1fseqlem5  23409  deg1ldgdomn  23775  drnguc1p  23851  quotval  23968  sincosq1sgn  24171  sincosq2sgn  24172  sincosq3sgn  24173  sincosq4sgn  24174  efabl  24217  lgsneg1  24964  dchrisumlem3  25097  ax5seglem2  25726  usgredg2vtx  26021  uspgredg2vtxeu  26022  usgredg2vtxeu  26023  cplgr3v  26235  vtxdumgr0nedg  26292  wlkwwlkinj  26668  wlkwwlksur  26669  clwlkclwwlk  26787  clwlksfclwwlk  26845  frgrncvvdeqlemB  27052  frgr2wsp1  27070  frrusgrord0  27078  grpocl  27224  grpodivcl  27263  ablomuldiv  27276  ablodivdiv4  27278  ablonnncan  27280  ablonnncan1  27282  vccl  27288  nvgcl  27345  nvcom  27346  nvadd4  27350  nvscl  27351  nvmval  27367  nvmcl  27371  nmcvcn  27420  nmlnoubi  27521  isblo3i  27526  blometi  27528  dipsubdir  27573  hlpar2  27622  hlpar  27623  hlcom  27626  hlipcj  27637  hlipgt0  27640  his52  27814  shintcli  28058  chlub  28238  homulass  28531  adjadj  28665  nmophmi  28760  kbass6  28850  atcvatlem  29114  mdsymlem3  29134  mdsymlem5  29136  rexdiv  29443  tltnle  29471  tlt3  29474  toslublem  29476  tosglblem  29478  archiabllem1b  29555  archiabllem2  29560  slmdacl  29571  slmdmcl  29572  slmdvacl  29574  aean  30112  fiunelcarsg  30183  probcun  30285  probdif  30287  cndprobin  30301  climuzcnv  31308  noprefixmo  31608  matunitlindflem1  33072  mblfinlem1  33113  mblfinlem2  33114  ftc1anclem6  33157  ssbnd  33254  heibor1  33276  exidcl  33342  rngocl  33367  rngogcl  33378  rngocom  33379  rngoa4  33382  rngosub  33396  rngonegmn1l  33407  rngonegmn1r  33408  ispridlc  33536  lshpcmp  33790  opltcon3b  34006  oldmm1  34019  olj01  34027  latm32  34033  omllaw4  34048  omllaw5N  34049  cmtcomlemN  34050  cmt2N  34052  cmtbr2N  34055  cmtbr3N  34056  cmtbr4N  34057  glbconxN  34179  hlexch1  34183  hlexch2  34184  hlexchb1  34185  hlexchb2  34186  hlexch3  34192  hlexch4N  34193  hlatexchb1  34194  hlatexchb2  34195  hlatexch1  34196  hlatexch2  34197  hlatle  34199  hlateq  34200  hlrelat1  34201  hlrelat2  34204  cvr1  34211  cvrval5  34216  cvrp  34217  atcvr1  34218  atcvr2  34219  cvrexchlem  34220  cvrexch  34221  dalem54  34527  pmaple  34562  pmap11  34563  paddass  34639  pmapj2N  34730  pmapocjN  34731  trlval2  34965  eelT00  38447  eelTTT  38448  eelT11  38449  eelT12  38451  eelTT1  38452  eelT01  38453  mullimc  39280  mullimcf  39287  stoweidlem52  39602  stoweidlem60  39610  rngcl  41197  nzerooringczr  41386  ply1mulgsum  41492  sinhpcosh  41800  reseccl  41813  recsccl  41814  recotcl  41815  onetansqsecsq  41821
  Copyright terms: Public domain W3C validator