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

Theorem syl3an1 1218
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 1141 . 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 937
This theorem is referenced by:  syl3an1b  1221  syl3an1br  1224  wefrc  4579  tz7.5  4605  fovrnda  6220  f1ofveu  6587  smoiso  6627  odi  6825  nndi  6869  nnmsucr  6871  f1oen2g  7127  f1dom2g  7128  domssex2  7270  ordunifi  7360  wemappo  7521  wemapso  7523  wemapso2  7524  ackbij1lem16  8120  divneg  9714  divdiv32  9727  divneg2  9743  ltdiv2  9900  fimaxre  9960  suprzcl  10354  peano2uz  10535  infmssuzle  10563  lbzbi  10569  zbtwnre  10577  irrmul  10604  supxrunb1  10903  expnlbnd  11514  retancl  12748  tanneg  12754  demoivreALT  12807  dvdscmulr  12883  dvdsmulcr  12884  gcd0id  13028  euclemma  13113  phiprmpw  13170  fermltl  13178  vdwapun  13347  vdwapid1  13348  pospo  14435  latasymb  14488  latjle12  14496  latlem12  14512  imasmnd2  14737  grpcl  14823  grprcan  14843  grpsubcl  14874  imasgrp2  14938  divsgrp  15000  ghmmulg  15023  ghmrn  15024  ghmeqker  15037  ablcom  15434  ablinvadd  15439  mulgmhm  15455  mulgghm  15456  odadd1  15468  odadd2  15469  rngcl  15682  crngcom  15683  rngacl  15696  imasrng  15730  irredlmul  15818  rhmmul  15833  drngmcl  15853  isdrngd  15865  subrgacl  15884  subrgugrp  15892  srngadd  15950  srngmul  15951  lmodacl  15966  lmodmcl  15967  lmodvacl  15969  lmodvsubcl  15994  lmod4  15999  lmodvaddsub4  16001  lmodvpncan  16002  lmodvnpcan  16003  lmodsubeq0  16008  islbs2  16231  islbs3  16232  lbsext  16240  rspssp  16302  mplbas2  16536  coe1add  16662  coe1subfv  16664  coe1mul2  16667  zlmlmod  16809  ipdir  16875  ip2eq  16889  ocvin  16906  filin  17891  filfinnfr  17914  filuni  17922  ufprim  17946  uffinfix  17964  hausflf  18034  uffcfflf  18076  cnextcn  18103  tmdmulg  18127  tsmsxplem1  18187  psmetcl  18343  xmetcl  18366  metcl  18367  meteq0  18374  metge0  18380  metsym  18385  metgt0  18394  blelrnps  18451  blelrn  18452  blssm  18453  blres  18466  mscl  18496  xmscl  18497  xmsge0  18498  xmseq0  18499  xmssym  18500  mopnin  18532  metustblOLD  18615  metutopOLD  18617  nmf2  18645  ngpdsr  18656  ngpds2  18657  ngpds2r  18658  ngpds3  18659  ngpds3r  18660  nmge0  18668  nmeq0  18669  nm2dif  18676  nmmul  18705  nlmmul0or  18724  nmods  18783  clmsub  19110  clmacl  19113  clmmcl  19114  clmsubcl  19115  cphnmvs  19158  cphipcl  19159  cphipcj  19167  cphorthcom  19168  fmcfil  19230  mbfi1fseqlem3  19612  mbfi1fseqlem4  19613  mbfi1fseqlem5  19614  evlsrhm  19947  deg1ldgdomn  20022  drnguc1p  20098  quotval  20214  sincosq1sgn  20411  sincosq2sgn  20412  sincosq3sgn  20413  sincosq4sgn  20414  lgsneg1  21109  dchrisumlem3  21190  wlkdvspthlem  21612  grpocl  21793  grpodivcl  21840  ablomuldiv  21882  ablodivdiv4  21884  ablonnncan  21886  ablonnncan1  21888  gxdi  21889  rngocl  21975  rngogcl  21984  rngocom  21985  rngoa4  21988  vccl  22034  vcgcl  22043  vccom  22044  vca4  22047  nvgcl  22104  nvcom  22105  nvadd4  22111  nvscl  22112  nvmval  22128  nvmcl  22133  nmcvcn  22196  nmlnoubi  22302  isblo3i  22307  blometi  22309  dipsubdir  22354  hlpar2  22403  hlpar  22404  hlcom  22407  hlipcj  22418  hlipgt0  22421  his52  22594  shintcli  22836  chlub  23016  homulass  23310  adjadj  23444  nmophmi  23539  kbass6  23629  atcvatlem  23893  mdsymlem3  23913  mdsymlem5  23915  rexdiv  24177  tltnle  24195  toslub  24196  tosglb  24197  aean  24600  probcun  24681  probdif  24683  cndprobin  24697  climuzcnv  25113  ax5seglem2  25873  mblfinlem1  26255  mblfinlem2  26256  ftc1anclem6  26299  ssbnd  26511  heibor1  26533  exidcl  26565  rngosub  26578  rngonegmn1l  26579  rngonegmn1r  26580  ispridlc  26694  pwssplit3  27181  frlmsplit2  27234  rngvcl  27444  stoweidlem52  27791  stoweidlem60  27799  frg2spot1  28521  frgregordn0  28533  sinhpcosh  28557  reseccl  28570  recsccl  28571  recotcl  28572  onetansqsecsq  28578  eelT00  28882  eelTTT  28883  eelT11  28885  eelT12  28889  eelTT1  28891  eelT01  28892  lshpcmp  29860  op0le  30058  ople1  30063  opltcon3b  30076  oldmm1  30089  olj01  30097  latm32  30103  omllaw4  30118  omllaw5N  30119  cmtcomlemN  30120  cmt2N  30122  cmtbr2N  30125  cmtbr3N  30126  cmtbr4N  30127  atl0le  30176  glbconxN  30249  hlexch1  30253  hlexch2  30254  hlexchb1  30255  hlexchb2  30256  hlexch3  30262  hlexch4N  30263  hlatexchb1  30264  hlatexchb2  30265  hlatexch1  30266  hlatexch2  30267  hlatle  30269  hlateq  30270  hlrelat1  30271  hlrelat2  30274  cvr1  30281  cvrval5  30286  cvrp  30287  atcvr1  30288  atcvr2  30289  cvrexchlem  30290  cvrexch  30291  dalem54  30597  pmaple  30632  pmap11  30633  paddass  30709  pmapj2N  30800  pmapocjN  30801  trlval2  31034
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 179  df-an 362  df-3an 939
  Copyright terms: Public domain W3C validator