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

Theorem syl3an1 1195
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 1184 . 2 ((𝜑𝜒𝜃) → (𝜓𝜒𝜃))
3 syl3an1.2 . 2 ((𝜓𝜒𝜃) → 𝜏)
42, 3syl 17 1 ((𝜑𝜒𝜃) → 𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1100
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 198  df-an 385  df-3an 1102
This theorem is referenced by:  3adant1l  1214  3adant1r  1216  syl3an1b  1515  syl3an1br  1518  wefrc  5312  tz7.5  5964  f1ofveu  6872  fovrnda  7038  smoiso  7698  odi  7899  nndi  7943  nnmsucr  7945  f1oen2g  8212  f1dom2g  8213  domssex2  8362  ordunifi  8452  wemappo  8696  wemapso  8698  ackbij1lem16  9345  divneg  11007  divdiv32  11021  divneg2  11037  ltdiv2  11197  fimaxre  11256  suprzcl  11726  peano2uz  11962  infssuzle  11993  lbzbi  11998  zbtwnre  12008  irrmul  12035  supxrunb1  12370  expnlbnd  13220  hash1to3  13493  fun2dmnop  13497  brfi1uzind  13500  brcnvtrclfvcnv  13972  retancl  15095  tanneg  15101  demoivreALT  15154  dvdscmulr  15236  dvdsmulcr  15237  mulmoddvds  15277  gcd0id  15462  euclemma  15645  phiprmpw  15701  fermltl  15709  vdwapun  15898  vdwapid1  15899  cshwshashlem1  16017  fsets  16105  pospo  17181  latasymb  17262  mndcl  17509  imasmnd2  17535  grpcl  17638  dfgrp2  17655  grprcan  17663  grpsubcl  17703  imasgrp2  17738  mhmid  17744  mhmmnd  17745  mulginvcom  17772  qusgrp  17854  ghmmulg  17877  ghmrn  17878  ghmeqker  17892  gsumccatsymgsn  18050  ablcom  18414  ablinvadd  18419  mulgmhm  18437  mulgghm  18438  ghmcmn  18441  odadd1  18455  odadd2  18456  srgcl  18717  srgacl  18729  srgcom  18730  ringcl  18766  crngcom  18767  ringacl  18783  imasring  18824  irredlmul  18913  rhmmul  18934  drngmcl  18967  isdrngd  18979  subrgacl  18998  subrgugrp  19006  srngadd  19064  srngmul  19065  idsrngd  19069  lmodacl  19081  lmodmcl  19082  lmodvacl  19084  lmodvsubcl  19115  lmod4  19120  lmodvaddsub4  19122  lmodvpncan  19123  lmodvnpcan  19124  lmodsubeq0  19129  pwssplit3  19271  islbs2  19366  islbs3  19367  lbsext  19375  rspssp  19438  mplbas2  19682  coe1add  19845  coe1subfv  19847  coe1mul2  19850  zlmlmod  20082  psgnco  20139  ipdir  20197  ip2eq  20211  ocvin  20232  frlmsplit2  20326  ringvcl  20418  cramer  20714  chpmat1d  20858  filin  21875  filfinnfr  21898  filuni  21906  ufprim  21930  uffinfix  21948  hausflf  22018  uffcfflf  22060  cnextcn  22088  tmdmulg  22113  tsmsxplem1  22173  psmetcl  22329  xmetcl  22353  metcl  22354  meteq0  22361  metge0  22367  metsym  22372  metgt0  22381  blelrnps  22438  blelrn  22439  blssm  22440  blres  22453  mscl  22483  xmscl  22484  xmsge0  22485  xmseq0  22486  xmssym  22487  mopnin  22519  nmf2  22614  ngpdsr  22626  ngpds2  22627  ngpds2r  22628  ngpds3  22629  ngpds3r  22630  nmge0  22638  nmeq0  22639  nm2dif  22646  nmmul  22685  nlmmul0or  22704  nmods  22765  clmsub  23096  clmacl  23100  clmmcl  23101  clmsubcl  23102  clmvscl  23104  clmvsubval  23125  ncvsprp  23168  ncvsdif  23171  ncvspds  23177  cphnmvs  23206  cphipcl  23207  cphipcj  23215  cphorthcom  23217  cphipval2  23256  4cphipval2  23257  cphipval  23258  fmcfil  23287  mbfi1fseqlem3  23704  mbfi1fseqlem4  23705  mbfi1fseqlem5  23706  deg1ldgdomn  24074  drnguc1p  24150  quotval  24267  sincosq1sgn  24471  sincosq2sgn  24472  sincosq3sgn  24473  sincosq4sgn  24474  efabl  24517  lgsneg1  25267  dchrisumlem3  25400  ax5seglem2  26029  usgredg2vtx  26332  uspgredg2vtxeu  26333  usgredg2vtxeu  26334  cplgr3v  26565  vtxdumgr0nedg  26623  wlkwwlkinjOLD  27030  wlkwwlksurOLD  27031  clwlkclwwlk  27151  clwlksfclwwlkOLD  27242  frgrncvvdeqlem8  27487  grpocl  27689  grpodivcl  27728  ablomuldiv  27741  ablodivdiv4  27743  ablonnncan1  27746  vccl  27752  nvgcl  27809  nvcom  27810  nvadd4  27814  nvscl  27815  nvmval  27831  nvmcl  27835  nmcvcn  27884  nmlnoubi  27985  isblo3i  27990  blometi  27992  dipsubdir  28037  hlpar2  28086  hlpar  28087  hlcom  28090  hlipcj  28101  hlipgt0  28104  his52  28278  shintcli  28522  chlub  28702  homulass  28995  adjadj  29129  nmophmi  29224  kbass6  29314  atcvatlem  29578  mdsymlem3  29598  mdsymlem5  29600  rexdiv  29965  tltnle  29993  tlt3  29996  toslublem  29998  tosglblem  30000  archiabllem1b  30077  archiabllem2  30082  slmdacl  30093  slmdmcl  30094  slmdvacl  30096  aean  30638  fiunelcarsg  30709  probcun  30811  probdif  30813  cndprobin  30827  climuzcnv  31892  matunitlindflem1  33720  mblfinlem1  33761  mblfinlem2  33762  ftc1anclem6  33804  ssbnd  33900  heibor1  33922  exidcl  33988  rngocl  34013  rngogcl  34024  rngocom  34025  rngoa4  34028  rngosub  34042  rngonegmn1l  34053  rngonegmn1r  34054  ispridlc  34182  lshpcmp  34770  opltcon3b  34986  oldmm1  34999  olj01  35007  latm32  35013  omllaw4  35028  omllaw5N  35029  cmtcomlemN  35030  cmt2N  35032  cmtbr2N  35035  cmtbr3N  35036  cmtbr4N  35037  glbconxN  35160  hlexch1  35164  hlexch2  35165  hlexchb1  35166  hlexchb2  35167  hlexch3  35173  hlexch4N  35174  hlatexchb1  35175  hlatexchb2  35176  hlatexch1  35177  hlatexch2  35178  hlatle  35180  hlateq  35181  hlrelat1  35182  hlrelat2  35185  cvr1  35192  cvrval5  35197  cvrp  35198  atcvr1  35199  atcvr2  35200  cvrexchlem  35201  cvrexch  35202  dalem54  35508  pmaple  35543  pmap11  35544  paddass  35620  pmapj2N  35711  pmapocjN  35712  trlval2  35945  eelT00  39429  eelTTT  39430  eelT11  39431  eelT12  39433  eelTT1  39434  eelT01  39435  mullimc  40329  mullimcf  40336  stoweidlem52  40749  stoweidlem60  40757  rngcl  42452  nzerooringczr  42641  ply1mulgsum  42747  sinhpcosh  43053  reseccl  43066  recsccl  43067  recotcl  43068  onetansqsecsq  43074
  Copyright terms: Public domain W3C validator