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

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

Proof of Theorem syl3an3
StepHypRef Expression
1 syl3an3.1 . . 3  |-  ( ph  ->  th )
2 syl3an3.2 . . . 4  |-  ( ( ps  /\  ch  /\  th )  ->  ta )
323exp 1205 . . 3  |-  ( ps 
->  ( ch  ->  ( th  ->  ta ) ) )
41, 3syl7 71 . 2  |-  ( ps 
->  ( ch  ->  ( ph  ->  ta ) ) )
543imp 1200 1  |-  ( ( ps  /\  ch  /\  ph )  ->  ta )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 983
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 189  df-an 373  df-3an 985
This theorem is referenced by:  syl3an3b  1303  syl3an3br  1306  vtoclgft  3130  disji  4409  ovmpt2x  6437  ovmpt2ga  6438  wfrlem14  7055  unbnn2  7832  axdc3lem4  8885  axdclem2  8952  gruiin  9237  gruen  9239  divass  10290  ltmul2  10458  xleadd1  11543  xltadd2  11545  xlemul1  11578  xltmul2  11581  elfzo  11924  modcyc2  12134  faclbnd5  12484  relexprel  13096  subcn2  13651  mulcn2  13652  ndvdsp1  14383  gcddiv  14510  lcmneg  14561  lubel  16361  gsumccatsn  16620  oddvdsi  17190  odcong  17191  odeq  17192  efgsp1  17380  lspsnss  18206  lindsmm2  19379  mulmarep1el  19589  mdetunilem4  19632  iuncld  20052  neips  20121  opnneip  20127  comppfsc  20539  hmeof1o2  20770  ordthmeo  20809  ufinffr  20936  elfm3  20957  utop3cls  21258  blcntrps  21419  blcntr  21420  neibl  21508  blnei  21509  metss  21515  stdbdmetval  21521  prdsms  21538  blval2  21569  lmmbr  22220  lmmbr2  22221  iscau2  22239  bcthlem1  22284  bcthlem3  22286  bcthlem4  22287  dvn2bss  22876  dvfsumrlim  22975  dvfsumrlim2  22976  cxpexpz  23604  cxpsub  23619  relogbzexp  23705  wlkcompim  25246  wwlknext  25444  wwlkextproplem3  25463  clwlkcompim  25484  clwwlkel  25513  clwwlkf  25514  numclwlk1lem2f1  25814  gxpval  25979  gxnn0neg  25983  gxnn0suc  25984  gxcl  25985  gxneg  25986  gxcom  25989  gxinv  25990  gxsuc  25992  gxnn0add  25994  gxadd  25995  gxsub  25996  gxnn0mul  25997  gxmul  25998  hvaddsub12  26683  hvaddsubass  26686  hvsubdistr1  26694  hvsubcan  26719  hhssnv  26907  spanunsni  27224  homco1  27446  homulass  27447  hoadddir  27449  hosubdi  27453  hoaddsubass  27460  hosubsub4  27463  lnopmi  27645  adjlnop  27731  mdsymlem5  28052  disjif  28184  disjif2  28187  ind0  28843  sigaclfu  28943  bnj544  29707  bnj561  29716  bnj562  29717  bnj594  29725  clsint2  30984  ftc1anclem6  31942  isbnd2  32035  blbnd  32039  isdrngo2  32117  atnem0  32809  hlrelat5N  32891  ltrnel  33629  ltrnat  33630  ltrncnvat  33631  jm2.22  35776  jm2.23  35777  dvconstbi  36547  eelT11  36954  eelT12  36958  eelTT1  36960  eelT01  36961  eel0T1  36962  rmfsupp  39465  mndpfsupp  39467  scmfsupp  39469  dignn0flhalflem2  39733
  Copyright terms: Public domain W3C validator