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

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

Proof of Theorem syl3an2
StepHypRef Expression
1 syl3an2.1 . . 3  |-  ( ph  ->  ch )
2 syl3an2.2 . . . 4  |-  ( ( ps  /\  ch  /\  th )  ->  ta )
323exp 1150 . . 3  |-  ( ps 
->  ( ch  ->  ( th  ->  ta ) ) )
41, 3syl5 28 . 2  |-  ( ps 
->  ( ph  ->  ( th  ->  ta ) ) )
543imp 1145 1  |-  ( ( ps  /\  ph  /\  th )  ->  ta )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 934
This theorem is referenced by:  syl3an2b  1219  syl3an2br  1222  syl3anl2  1231  odi  6577  omass  6578  nndi  6621  nnmass  6622  omabslem  6644  winainf  8316  divsubdir  9456  divdiv32  9468  ltdiv2  9641  peano2uz  10272  irrmul  10341  supxrunb1  10638  axdc4uzlem  11044  expdiv  11152  bcval5  11330  cats1un  11476  rediv  11616  imdiv  11623  absdiflt  11801  absdifle  11802  iseraltlem3  12156  retancl  12422  tanneg  12428  prmdvdsexpb  12794  lspssp  15745  islp2  16877  fmfg  17644  fmufil  17654  flffbas  17690  lmflf  17700  uffcfflf  17734  blres  17977  caucfil  18709  deg1mul3  19501  quotval  19672  gxid  20940  nvsge0  21229  hvsubass  21623  hvsubdistr2  21629  hvsubcan  21653  his2sub  21671  chlub  22088  spanunsni  22158  homco1  22381  homulass  22382  cnlnadjlem2  22648  adjmul  22672  chirredlem2  22971  atmd2  22980  mdsymlem5  22987  climuzcnv  24004  clfsebs3  25380  clfsebs4  25381  clfsebs5  25382  mulveczer  25479  cmp2morpdom  25964  f1ocan2fv  26395  isdrngo2  26589  eluzrabdioph  26887  pmtrfb  27406  dvconstbi  27551  sinhpcosh  28210  reseccl  28223  recsccl  28224  recotcl  28225  onetansqsecsq  28231  eelT11  28483  eelT12  28486  eelTT1  28488  eel0T1  28490  atncvrN  29505  cvlatcvr1  29531
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 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator