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

Theorem syl3an3 1248
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 1181 . . 3  |-  ( ps 
->  ( ch  ->  ( th  ->  ta ) ) )
41, 3syl7 68 . 2  |-  ( ps 
->  ( ch  ->  ( ph  ->  ta ) ) )
543imp 1176 1  |-  ( ( ps  /\  ch  /\  ph )  ->  ta )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 960
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 185  df-an 371  df-3an 962
This theorem is referenced by:  syl3an3b  1251  syl3an3br  1254  vtoclgft  3017  disji  4277  ovmpt2x  6218  ovmpt2ga  6219  unbnn2  7565  axdc3lem4  8618  axdclem2  8685  gruiin  8973  gruen  8975  divass  10008  ltmul2  10176  xleadd1  11214  xltadd2  11216  xlemul1  11249  xltmul2  11252  elfzo  11551  modcyc2  11740  faclbnd5  12070  subcn2  13068  mulcn2  13069  ndvdsp1  13609  gcddiv  13729  lubel  15288  gsumccatsn  15514  oddvdsi  16044  odcong  16045  odeq  16046  efgsp1  16227  lspsnss  17049  lindsmm2  18217  mulmarep1el  18342  mdetunilem4  18380  iuncld  18608  neips  18676  opnneip  18682  hmeof1o2  19295  ordthmeo  19334  ufinffr  19461  elfm3  19482  utop3cls  19785  blcntrps  19946  blcntr  19947  neibl  20035  blnei  20036  metss  20042  stdbdmetval  20048  prdsms  20065  blval2  20109  lmmbr  20728  lmmbr2  20729  iscau2  20747  bcthlem1  20794  bcthlem3  20796  bcthlem4  20797  dvn2bss  21363  dvfsumrlim  21462  dvfsumrlim2  21463  cxpexpz  22071  cxpsub  22086  2pthon  23436  gxpval  23681  gxnn0neg  23685  gxnn0suc  23686  gxcl  23687  gxneg  23688  gxcom  23691  gxinv  23692  gxsuc  23694  gxnn0add  23696  gxadd  23697  gxsub  23698  gxnn0mul  23699  gxmul  23700  hvaddsub12  24375  hvaddsubass  24378  hvsubdistr1  24386  hvsubcan  24411  hhssnv  24600  spanunsni  24917  homco1  25140  homulass  25141  hoadddir  25143  hosubdi  25147  hoaddsubass  25154  hosubsub4  25157  lnopmi  25339  adjlnop  25425  mdsymlem5  25746  disjif  25857  disjif2  25860  ind0  26412  sigaclfu  26498  wfrlem14  27666  ftc1anclem6  28397  clsint2  28449  comppfsc  28504  isbnd2  28607  blbnd  28611  isdrngo2  28689  jm2.22  29269  jm2.23  29270  dvconstbi  29533  wlkcompim  30212  wwlknext  30281  clwlkcompim  30352  clwwlkel  30380  clwwlkf  30381  wwlkextproplem3  30487  numclwlk1lem2f1  30612  rmfsupp  30704  mndpfsupp  30706  scmfsupp  30708  eelT11  31266  eelT12  31270  eelTT1  31272  eelT01  31273  eel0T1  31274  bnj544  31721  bnj561  31730  bnj562  31731  bnj594  31739  atnem0  32685  hlrelat5N  32767  ltrnel  33505  ltrnat  33506  ltrncnvat  33507
  Copyright terms: Public domain W3C validator