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  6593  omass  6594  nndi  6637  nnmass  6638  omabslem  6660  winainf  8332  divsubdir  9472  divdiv32  9484  ltdiv2  9657  peano2uz  10288  irrmul  10357  supxrunb1  10654  axdc4uzlem  11060  expdiv  11168  bcval5  11346  cats1un  11492  rediv  11632  imdiv  11639  absdiflt  11817  absdifle  11818  iseraltlem3  12172  retancl  12438  tanneg  12444  prmdvdsexpb  12810  lspssp  15761  islp2  16893  fmfg  17660  fmufil  17670  flffbas  17706  lmflf  17716  uffcfflf  17750  blres  17993  caucfil  18725  deg1mul3  19517  quotval  19688  gxid  20956  nvsge0  21245  hvsubass  21639  hvsubdistr2  21645  hvsubcan  21669  his2sub  21687  chlub  22104  spanunsni  22174  homco1  22397  homulass  22398  cnlnadjlem2  22664  adjmul  22688  chirredlem2  22987  atmd2  22996  mdsymlem5  23003  climuzcnv  24019  clfsebs3  25483  clfsebs4  25484  clfsebs5  25485  mulveczer  25582  cmp2morpdom  26067  f1ocan2fv  26498  isdrngo2  26692  eluzrabdioph  26990  pmtrfb  27509  dvconstbi  27654  cusgra3vnbpr  28300  sinhpcosh  28464  reseccl  28477  recsccl  28478  recotcl  28479  onetansqsecsq  28485  eelT11  28788  eelT12  28792  eelTT1  28794  eel0T1  28796  atncvrN  30127  cvlatcvr1  30153
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