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

Theorem syl3an3 1263
Description: A syllogism inference. (Contributed by NM, 22-Aug-1995.)
Hypotheses
Ref Expression
syl3an3.1
syl3an3.2
Assertion
Ref Expression
syl3an3

Proof of Theorem syl3an3
StepHypRef Expression
1 syl3an3.1 . . 3
2 syl3an3.2 . . . 4
323exp 1195 . . 3
41, 3syl7 68 . 2
543imp 1190 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\w3a 973
This theorem is referenced by:  syl3an3b  1266  syl3an3br  1269  vtoclgft  3157  disji  4440  ovmpt2x  6431  ovmpt2ga  6432  unbnn2  7797  axdc3lem4  8854  axdclem2  8921  gruiin  9209  gruen  9211  divass  10250  ltmul2  10418  xleadd1  11476  xltadd2  11478  xlemul1  11511  xltmul2  11514  elfzo  11831  modcyc2  12032  faclbnd5  12376  subcn2  13417  mulcn2  13418  ndvdsp1  14067  gcddiv  14187  lubel  15752  gsumccatsn  16011  oddvdsi  16572  odcong  16573  odeq  16574  efgsp1  16755  lspsnss  17636  lindsmm2  18864  mulmarep1el  19074  mdetunilem4  19117  iuncld  19546  neips  19614  opnneip  19620  comppfsc  20033  hmeof1o2  20264  ordthmeo  20303  ufinffr  20430  elfm3  20451  utop3cls  20754  blcntrps  20915  blcntr  20916  neibl  21004  blnei  21005  metss  21011  stdbdmetval  21017  prdsms  21034  blval2  21078  lmmbr  21697  lmmbr2  21698  iscau2  21716  bcthlem1  21763  bcthlem3  21765  bcthlem4  21766  dvn2bss  22333  dvfsumrlim  22432  dvfsumrlim2  22433  cxpexpz  23048  cxpsub  23063  wlkcompim  24526  wwlknext  24724  wwlkextproplem3  24743  clwlkcompim  24764  clwwlkel  24793  clwwlkf  24794  numclwlk1lem2f1  25094  gxpval  25261  gxnn0neg  25265  gxnn0suc  25266  gxcl  25267  gxneg  25268  gxcom  25271  gxinv  25272  gxsuc  25274  gxnn0add  25276  gxadd  25277  gxsub  25278  gxnn0mul  25279  gxmul  25280  hvaddsub12  25955  hvaddsubass  25958  hvsubdistr1  25966  hvsubcan  25991  hhssnv  26180  spanunsni  26497  homco1  26720  homulass  26721  hoadddir  26723  hosubdi  26727  hoaddsubass  26734  hosubsub4  26737  lnopmi  26919  adjlnop  27005  mdsymlem5  27326  disjif  27439  disjif2  27442  ind0  28033  sigaclfu  28119  wfrlem14  29356  ftc1anclem6  30095  clsint2  30147  isbnd2  30279  blbnd  30283  isdrngo2  30361  jm2.22  30937  jm2.23  30938  lcmneg  31209  dvconstbi  31239  rmfsupp  32967  mndpfsupp  32969  scmfsupp  32971  eelT11  33496  eelT12  33500  eelTT1  33502  eelT01  33503  eel0T1  33504  bnj544  33952  bnj561  33961  bnj562  33962  bnj594  33970  atnem0  35043  hlrelat5N  35125  ltrnel  35863  ltrnat  35864  ltrncnvat  35865
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 975
  Copyright terms: Public domain W3C validator