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

Theorem syl3an2 1218
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 1152 . . 3  |-  ( ps 
->  ( ch  ->  ( th  ->  ta ) ) )
41, 3syl5 30 . 2  |-  ( ps 
->  ( ph  ->  ( th  ->  ta ) ) )
543imp 1147 1  |-  ( ( ps  /\  ph  /\  th )  ->  ta )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 936
This theorem is referenced by:  syl3an2b  1221  syl3an2br  1224  syl3anl2  1233  odi  6822  omass  6823  nndi  6866  nnmass  6867  omabslem  6889  winainf  8569  divsubdir  9710  divdiv32  9722  ltdiv2  9895  peano2uz  10530  irrmul  10599  supxrunb1  10898  axdc4uzlem  11321  expdiv  11430  bcval5  11609  cats1un  11790  rediv  11936  imdiv  11943  absdiflt  12121  absdifle  12122  iseraltlem3  12477  retancl  12743  tanneg  12749  prmdvdsexpb  13115  lspssp  16064  islp2  17209  fmfg  17981  fmufil  17991  flffbas  18027  lmflf  18037  uffcfflf  18071  blres  18461  caucfil  19236  cmetcusp1OLD  19305  cmetcusp1  19306  deg1mul3  20038  quotval  20209  cusgra3vnbpr  21474  gxid  21861  nvsge0  22152  hvsubass  22546  hvsubdistr2  22552  hvsubcan  22576  his2sub  22594  chlub  23011  spanunsni  23081  homco1  23304  homulass  23305  cnlnadjlem2  23571  adjmul  23595  chirredlem2  23894  atmd2  23903  mdsymlem5  23910  climuzcnv  25108  f1ocan2fv  26429  isdrngo2  26574  eluzrabdioph  26866  pmtrfb  27383  dvconstbi  27528  ltdifltdiv  28148  sinhpcosh  28483  reseccl  28496  recsccl  28497  recotcl  28498  onetansqsecsq  28504  eelT11  28811  eelT12  28815  eelTT1  28817  eel0T1  28819  atncvrN  30113  cvlatcvr1  30139
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