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

Theorem syl3an1 1217
Description: A syllogism inference. (Contributed by NM, 22-Aug-1995.)
Hypotheses
Ref Expression
syl3an1.1  |-  ( ph  ->  ps )
syl3an1.2  |-  ( ( ps  /\  ch  /\  th )  ->  ta )
Assertion
Ref Expression
syl3an1  |-  ( (
ph  /\  ch  /\  th )  ->  ta )

Proof of Theorem syl3an1
StepHypRef Expression
1 syl3an1.1 . . 3  |-  ( ph  ->  ps )
213anim1i 1140 . 2  |-  ( (
ph  /\  ch  /\  th )  ->  ( ps  /\  ch  /\  th ) )
3 syl3an1.2 . 2  |-  ( ( ps  /\  ch  /\  th )  ->  ta )
42, 3syl 16 1  |-  ( (
ph  /\  ch  /\  th )  ->  ta )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 936
This theorem is referenced by:  syl3an1b  1220  syl3an1br  1223  wefrc  4536  tz7.5  4562  fovrnda  6176  f1ofveu  6543  smoiso  6583  odi  6781  nndi  6825  nnmsucr  6827  f1oen2g  7083  f1dom2g  7084  domssex2  7226  ordunifi  7316  wemappo  7474  wemapso  7476  wemapso2  7477  ackbij1lem16  8071  divneg  9665  divdiv32  9678  divneg2  9694  ltdiv2  9851  fimaxre  9911  suprzcl  10305  peano2uz  10486  infmssuzle  10514  lbzbi  10520  zbtwnre  10528  irrmul  10555  supxrunb1  10854  expnlbnd  11464  retancl  12698  tanneg  12704  demoivreALT  12757  dvdscmulr  12833  dvdsmulcr  12834  gcd0id  12978  euclemma  13063  phiprmpw  13120  fermltl  13128  vdwapun  13297  vdwapid1  13298  pospo  14385  latasymb  14438  latjle12  14446  latlem12  14462  imasmnd2  14687  grpcl  14773  grprcan  14793  grpsubcl  14824  imasgrp2  14888  divsgrp  14950  ghmmulg  14973  ghmrn  14974  ghmeqker  14987  ablcom  15384  ablinvadd  15389  mulgmhm  15405  mulgghm  15406  odadd1  15418  odadd2  15419  rngcl  15632  crngcom  15633  rngacl  15646  imasrng  15680  irredlmul  15768  rhmmul  15783  drngmcl  15803  isdrngd  15815  subrgacl  15834  subrgugrp  15842  srngadd  15900  srngmul  15901  lmodacl  15916  lmodmcl  15917  lmodvacl  15919  lmodvsubcl  15944  lmod4  15949  lmodvaddsub4  15951  lmodvpncan  15952  lmodvnpcan  15953  lmodsubeq0  15958  islbs2  16181  islbs3  16182  lbsext  16190  rspssp  16252  mplbas2  16486  coe1add  16612  coe1subfv  16614  coe1mul2  16617  zlmlmod  16759  ipdir  16825  ip2eq  16839  ocvin  16856  filin  17839  filfinnfr  17862  filuni  17870  ufprim  17894  uffinfix  17912  hausflf  17982  uffcfflf  18024  cnextcn  18051  tmdmulg  18075  tsmsxplem1  18135  psmetcl  18291  xmetcl  18314  metcl  18315  meteq0  18322  metge0  18328  metsym  18333  metgt0  18342  blelrnps  18399  blelrn  18400  blssm  18401  blres  18414  mscl  18444  xmscl  18445  xmsge0  18446  xmseq0  18447  xmssym  18448  mopnin  18480  metustblOLD  18563  metutopOLD  18565  nmf2  18593  ngpdsr  18604  ngpds2  18605  ngpds2r  18606  ngpds3  18607  ngpds3r  18608  nmge0  18616  nmeq0  18617  nm2dif  18624  nmmul  18653  nlmmul0or  18672  nmods  18731  clmsub  19058  clmacl  19061  clmmcl  19062  clmsubcl  19063  cphnmvs  19106  cphipcl  19107  cphipcj  19115  cphorthcom  19116  fmcfil  19178  mbfi1fseqlem3  19562  mbfi1fseqlem4  19563  mbfi1fseqlem5  19564  evlsrhm  19895  deg1ldgdomn  19970  drnguc1p  20046  quotval  20162  sincosq1sgn  20359  sincosq2sgn  20360  sincosq3sgn  20361  sincosq4sgn  20362  lgsneg1  21057  dchrisumlem3  21138  wlkdvspthlem  21560  grpocl  21741  grpodivcl  21788  ablomuldiv  21830  ablodivdiv4  21832  ablonnncan  21834  ablonnncan1  21836  gxdi  21837  rngocl  21923  rngogcl  21932  rngocom  21933  rngoa4  21936  vccl  21982  vcgcl  21991  vccom  21992  vca4  21995  nvgcl  22052  nvcom  22053  nvadd4  22059  nvscl  22060  nvmval  22076  nvmcl  22081  nmcvcn  22144  nmlnoubi  22250  isblo3i  22255  blometi  22257  dipsubdir  22302  hlpar2  22351  hlpar  22352  hlcom  22355  hlipcj  22366  hlipgt0  22369  his52  22542  shintcli  22784  chlub  22964  homulass  23258  adjadj  23392  nmophmi  23487  kbass6  23577  atcvatlem  23841  mdsymlem3  23861  mdsymlem5  23863  rexdiv  24125  tltnle  24143  toslub  24144  tosglb  24145  aean  24548  probcun  24629  probdif  24631  cndprobin  24645  climuzcnv  25061  ax5seglem2  25772  mblfinlem  26143  ssbnd  26387  heibor1  26409  exidcl  26441  rngosub  26454  rngonegmn1l  26455  rngonegmn1r  26456  ispridlc  26570  pwssplit3  27058  frlmsplit2  27111  rngvcl  27321  stoweidlem52  27668  stoweidlem60  27676  frg2spot1  28161  frgregordn0  28173  sinhpcosh  28197  reseccl  28210  recsccl  28211  recotcl  28212  onetansqsecsq  28218  eelT00  28517  eelTTT  28518  eelT11  28520  eelT12  28524  eelTT1  28526  eelT01  28527  lshpcmp  29471  op0le  29669  ople1  29674  opltcon3b  29687  oldmm1  29700  olj01  29708  latm32  29714  omllaw4  29729  omllaw5N  29730  cmtcomlemN  29731  cmt2N  29733  cmtbr2N  29736  cmtbr3N  29737  cmtbr4N  29738  atl0le  29787  glbconxN  29860  hlexch1  29864  hlexch2  29865  hlexchb1  29866  hlexchb2  29867  hlexch3  29873  hlexch4N  29874  hlatexchb1  29875  hlatexchb2  29876  hlatexch1  29877  hlatexch2  29878  hlatle  29880  hlateq  29881  hlrelat1  29882  hlrelat2  29885  cvr1  29892  cvrval5  29897  cvrp  29898  atcvr1  29899  atcvr2  29900  cvrexchlem  29901  cvrexch  29902  dalem54  30208  pmaple  30243  pmap11  30244  paddass  30320  pmapj2N  30411  pmapocjN  30412  trlval2  30645
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator