MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl3an1 Structured version   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  4568  tz7.5  4594  fovrnda  6209  f1ofveu  6576  smoiso  6616  odi  6814  nndi  6858  nnmsucr  6860  f1oen2g  7116  f1dom2g  7117  domssex2  7259  ordunifi  7349  wemappo  7510  wemapso  7512  wemapso2  7513  ackbij1lem16  8107  divneg  9701  divdiv32  9714  divneg2  9730  ltdiv2  9887  fimaxre  9947  suprzcl  10341  peano2uz  10522  infmssuzle  10550  lbzbi  10556  zbtwnre  10564  irrmul  10591  supxrunb1  10890  expnlbnd  11501  retancl  12735  tanneg  12741  demoivreALT  12794  dvdscmulr  12870  dvdsmulcr  12871  gcd0id  13015  euclemma  13100  phiprmpw  13157  fermltl  13165  vdwapun  13334  vdwapid1  13335  pospo  14422  latasymb  14475  latjle12  14483  latlem12  14499  imasmnd2  14724  grpcl  14810  grprcan  14830  grpsubcl  14861  imasgrp2  14925  divsgrp  14987  ghmmulg  15010  ghmrn  15011  ghmeqker  15024  ablcom  15421  ablinvadd  15426  mulgmhm  15442  mulgghm  15443  odadd1  15455  odadd2  15456  rngcl  15669  crngcom  15670  rngacl  15683  imasrng  15717  irredlmul  15805  rhmmul  15820  drngmcl  15840  isdrngd  15852  subrgacl  15871  subrgugrp  15879  srngadd  15937  srngmul  15938  lmodacl  15953  lmodmcl  15954  lmodvacl  15956  lmodvsubcl  15981  lmod4  15986  lmodvaddsub4  15988  lmodvpncan  15989  lmodvnpcan  15990  lmodsubeq0  15995  islbs2  16218  islbs3  16219  lbsext  16227  rspssp  16289  mplbas2  16523  coe1add  16649  coe1subfv  16651  coe1mul2  16654  zlmlmod  16796  ipdir  16862  ip2eq  16876  ocvin  16893  filin  17878  filfinnfr  17901  filuni  17909  ufprim  17933  uffinfix  17951  hausflf  18021  uffcfflf  18063  cnextcn  18090  tmdmulg  18114  tsmsxplem1  18174  psmetcl  18330  xmetcl  18353  metcl  18354  meteq0  18361  metge0  18367  metsym  18372  metgt0  18381  blelrnps  18438  blelrn  18439  blssm  18440  blres  18453  mscl  18483  xmscl  18484  xmsge0  18485  xmseq0  18486  xmssym  18487  mopnin  18519  metustblOLD  18602  metutopOLD  18604  nmf2  18632  ngpdsr  18643  ngpds2  18644  ngpds2r  18645  ngpds3  18646  ngpds3r  18647  nmge0  18655  nmeq0  18656  nm2dif  18663  nmmul  18692  nlmmul0or  18711  nmods  18770  clmsub  19097  clmacl  19100  clmmcl  19101  clmsubcl  19102  cphnmvs  19145  cphipcl  19146  cphipcj  19154  cphorthcom  19155  fmcfil  19217  mbfi1fseqlem3  19601  mbfi1fseqlem4  19602  mbfi1fseqlem5  19603  evlsrhm  19934  deg1ldgdomn  20009  drnguc1p  20085  quotval  20201  sincosq1sgn  20398  sincosq2sgn  20399  sincosq3sgn  20400  sincosq4sgn  20401  lgsneg1  21096  dchrisumlem3  21177  wlkdvspthlem  21599  grpocl  21780  grpodivcl  21827  ablomuldiv  21869  ablodivdiv4  21871  ablonnncan  21873  ablonnncan1  21875  gxdi  21876  rngocl  21962  rngogcl  21971  rngocom  21972  rngoa4  21975  vccl  22021  vcgcl  22030  vccom  22031  vca4  22034  nvgcl  22091  nvcom  22092  nvadd4  22098  nvscl  22099  nvmval  22115  nvmcl  22120  nmcvcn  22183  nmlnoubi  22289  isblo3i  22294  blometi  22296  dipsubdir  22341  hlpar2  22390  hlpar  22391  hlcom  22394  hlipcj  22405  hlipgt0  22408  his52  22581  shintcli  22823  chlub  23003  homulass  23297  adjadj  23431  nmophmi  23526  kbass6  23616  atcvatlem  23880  mdsymlem3  23900  mdsymlem5  23902  rexdiv  24164  tltnle  24182  toslub  24183  tosglb  24184  aean  24587  probcun  24668  probdif  24670  cndprobin  24684  climuzcnv  25100  ax5seglem2  25860  mblfinlem  26234  ftc1anclem6  26275  ssbnd  26488  heibor1  26510  exidcl  26542  rngosub  26555  rngonegmn1l  26556  rngonegmn1r  26557  ispridlc  26671  pwssplit3  27158  frlmsplit2  27211  rngvcl  27421  stoweidlem52  27768  stoweidlem60  27776  frg2spot1  28384  frgregordn0  28396  sinhpcosh  28420  reseccl  28433  recsccl  28434  recotcl  28435  onetansqsecsq  28441  eelT00  28745  eelTTT  28746  eelT11  28748  eelT12  28752  eelTT1  28754  eelT01  28755  lshpcmp  29723  op0le  29921  ople1  29926  opltcon3b  29939  oldmm1  29952  olj01  29960  latm32  29966  omllaw4  29981  omllaw5N  29982  cmtcomlemN  29983  cmt2N  29985  cmtbr2N  29988  cmtbr3N  29989  cmtbr4N  29990  atl0le  30039  glbconxN  30112  hlexch1  30116  hlexch2  30117  hlexchb1  30118  hlexchb2  30119  hlexch3  30125  hlexch4N  30126  hlatexchb1  30127  hlatexchb2  30128  hlatexch1  30129  hlatexch2  30130  hlatle  30132  hlateq  30133  hlrelat1  30134  hlrelat2  30137  cvr1  30144  cvrval5  30149  cvrp  30150  atcvr1  30151  atcvr2  30152  cvrexchlem  30153  cvrexch  30154  dalem54  30460  pmaple  30495  pmap11  30496  paddass  30572  pmapj2N  30663  pmapocjN  30664  trlval2  30897
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