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

Theorem syl3an1 1399
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 1267 . 2 ((𝜑𝜒𝜃) → (𝜓𝜒𝜃))
3 syl3an1.2 . 2 ((𝜓𝜒𝜃) → 𝜏)
42, 3syl 17 1 ((𝜑𝜒𝜃) → 𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1054
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 385  df-3an 1056
This theorem is referenced by:  syl3an1b  1402  syl3an1br  1405  wefrc  5137  tz7.5  5782  f1ofveu  6685  fovrnda  6847  smoiso  7504  odi  7704  nndi  7748  nnmsucr  7750  f1oen2g  8014  f1dom2g  8015  domssex2  8161  ordunifi  8251  wemappo  8495  wemapso  8497  ackbij1lem16  9095  divneg  10757  divdiv32  10771  divneg2  10787  ltdiv2  10947  fimaxre  11006  suprzcl  11495  peano2uz  11779  infssuzle  11809  lbzbi  11814  zbtwnre  11824  irrmul  11851  supxrunb1  12187  expnlbnd  13034  hash1to3  13311  fun2dmnop  13315  brfi1uzind  13318  brcnvtrclfvcnv  13790  retancl  14916  tanneg  14922  demoivreALT  14975  dvdscmulr  15057  dvdsmulcr  15058  mulmoddvds  15098  gcd0id  15287  euclemma  15472  phiprmpw  15528  fermltl  15536  vdwapun  15725  vdwapid1  15726  cshwshashlem1  15849  fsets  15938  pospo  17020  latasymb  17101  mndcl  17348  imasmnd2  17374  grpcl  17477  dfgrp2  17494  grprcan  17502  grpsubcl  17542  imasgrp2  17577  mhmid  17583  mhmmnd  17584  mulginvcom  17612  qusgrp  17696  ghmmulg  17719  ghmrn  17720  ghmeqker  17734  gsumccatsymgsn  17892  ablcom  18256  ablinvadd  18261  mulgmhm  18279  mulgghm  18280  ghmcmn  18283  odadd1  18297  odadd2  18298  srgcl  18558  srgacl  18570  srgcom  18571  ringcl  18607  crngcom  18608  ringacl  18624  imasring  18665  irredlmul  18754  rhmmul  18775  drngmcl  18808  isdrngd  18820  subrgacl  18839  subrgugrp  18847  srngadd  18905  srngmul  18906  idsrngd  18910  lmodacl  18922  lmodmcl  18923  lmodvacl  18925  lmodvsubcl  18956  lmod4  18961  lmodvaddsub4  18963  lmodvpncan  18964  lmodvnpcan  18965  lmodsubeq0  18970  pwssplit3  19109  islbs2  19202  islbs3  19203  lbsext  19211  rspssp  19274  mplbas2  19518  coe1add  19682  coe1subfv  19684  coe1mul2  19687  zlmlmod  19919  psgnco  19977  ipdir  20032  ip2eq  20046  ocvin  20066  frlmsplit2  20160  ringvcl  20252  cramer  20545  chpmat1d  20689  filin  21705  filfinnfr  21728  filuni  21736  ufprim  21760  uffinfix  21778  hausflf  21848  uffcfflf  21890  cnextcn  21918  tmdmulg  21943  tsmsxplem1  22003  psmetcl  22159  xmetcl  22183  metcl  22184  meteq0  22191  metge0  22197  metsym  22202  metgt0  22211  blelrnps  22268  blelrn  22269  blssm  22270  blres  22283  mscl  22313  xmscl  22314  xmsge0  22315  xmseq0  22316  xmssym  22317  mopnin  22349  nmf2  22444  ngpdsr  22456  ngpds2  22457  ngpds2r  22458  ngpds3  22459  ngpds3r  22460  nmge0  22468  nmeq0  22469  nm2dif  22476  nmmul  22515  nlmmul0or  22534  nmods  22595  clmsub  22926  clmacl  22930  clmmcl  22931  clmsubcl  22932  clmvscl  22934  clmvsubval  22955  ncvsprp  22998  ncvsdif  23001  ncvspds  23007  cphnmvs  23036  cphipcl  23037  cphipcj  23045  cphorthcom  23047  cphipval2  23086  4cphipval2  23087  cphipval  23088  fmcfil  23116  mbfi1fseqlem3  23529  mbfi1fseqlem4  23530  mbfi1fseqlem5  23531  deg1ldgdomn  23899  drnguc1p  23975  quotval  24092  sincosq1sgn  24295  sincosq2sgn  24296  sincosq3sgn  24297  sincosq4sgn  24298  efabl  24341  lgsneg1  25092  dchrisumlem3  25225  ax5seglem2  25854  usgredg2vtx  26156  uspgredg2vtxeu  26157  usgredg2vtxeu  26158  cplgr3v  26387  vtxdumgr0nedg  26445  wlkwwlkinj  26850  wlkwwlksur  26851  clwlkclwwlk  26968  clwlksfclwwlk  27049  frgrncvvdeqlem8  27286  grpocl  27482  grpodivcl  27521  ablomuldiv  27534  ablodivdiv4  27536  ablonnncan  27538  ablonnncan1  27540  vccl  27546  nvgcl  27603  nvcom  27604  nvadd4  27608  nvscl  27609  nvmval  27625  nvmcl  27629  nmcvcn  27678  nmlnoubi  27779  isblo3i  27784  blometi  27786  dipsubdir  27831  hlpar2  27880  hlpar  27881  hlcom  27884  hlipcj  27895  hlipgt0  27898  his52  28072  shintcli  28316  chlub  28496  homulass  28789  adjadj  28923  nmophmi  29018  kbass6  29108  atcvatlem  29372  mdsymlem3  29392  mdsymlem5  29394  rexdiv  29762  tltnle  29790  tlt3  29793  toslublem  29795  tosglblem  29797  archiabllem1b  29874  archiabllem2  29879  slmdacl  29890  slmdmcl  29891  slmdvacl  29893  aean  30435  fiunelcarsg  30506  probcun  30608  probdif  30610  cndprobin  30624  climuzcnv  31691  matunitlindflem1  33535  mblfinlem1  33576  mblfinlem2  33577  ftc1anclem6  33620  ssbnd  33717  heibor1  33739  exidcl  33805  rngocl  33830  rngogcl  33841  rngocom  33842  rngoa4  33845  rngosub  33859  rngonegmn1l  33870  rngonegmn1r  33871  ispridlc  33999  lshpcmp  34593  opltcon3b  34809  oldmm1  34822  olj01  34830  latm32  34836  omllaw4  34851  omllaw5N  34852  cmtcomlemN  34853  cmt2N  34855  cmtbr2N  34858  cmtbr3N  34859  cmtbr4N  34860  glbconxN  34982  hlexch1  34986  hlexch2  34987  hlexchb1  34988  hlexchb2  34989  hlexch3  34995  hlexch4N  34996  hlatexchb1  34997  hlatexchb2  34998  hlatexch1  34999  hlatexch2  35000  hlatle  35002  hlateq  35003  hlrelat1  35004  hlrelat2  35007  cvr1  35014  cvrval5  35019  cvrp  35020  atcvr1  35021  atcvr2  35022  cvrexchlem  35023  cvrexch  35024  dalem54  35330  pmaple  35365  pmap11  35366  paddass  35442  pmapj2N  35533  pmapocjN  35534  trlval2  35768  eelT00  39247  eelTTT  39248  eelT11  39249  eelT12  39251  eelTT1  39252  eelT01  39253  mullimc  40166  mullimcf  40173  stoweidlem52  40587  stoweidlem60  40595  rngcl  42208  nzerooringczr  42397  ply1mulgsum  42503  sinhpcosh  42809  reseccl  42822  recsccl  42823  recotcl  42824  onetansqsecsq  42830
  Copyright terms: Public domain W3C validator