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

Theorem sylan2b 475
Description: A syllogism inference. (Contributed by NM, 21-Apr-1994.)
Hypotheses
Ref Expression
sylan2b.1
sylan2b.2
Assertion
Ref Expression
sylan2b

Proof of Theorem sylan2b
StepHypRef Expression
1 sylan2b.1 . . 3
21biimpi 194 . 2
3 sylan2b.2 . 2
42, 3sylan2 474 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  /\wa 369
This theorem is referenced by:  syl2anb  479  bianir  967  eupickb  2360  bm1.1OLD  2441  eqtr3  2485  elnelne1  2804  elnelne2  2805  morex  3283  psssstr  3609  reuss2  3777  reupick  3781  reximdva0  3796  rabsneu  4105  opabss  4513  triun  4558  poirr  4816  wefrc  4878  xpcan  5448  fnfco  5755  suppssrOLD  6021  fnressn  6083  fvtp3  6120  fvtp3g  6123  f1mpt  6169  offval  6547  ordsucuniel  6659  onzsl  6681  soex  6743  fun11iun  6760  dfoprab3  6856  1stconst  6888  2ndconst  6889  poxp  6912  fnwelem  6915  suppssr  6950  suppsssn  6954  oeordsuc  7262  oelim2  7263  omsmolem  7321  fisucdomOLD  7743  ssnnfi  7759  fiint  7817  unifi  7829  indexfi  7848  iinfi  7897  unwdomg  8031  inf3lem5  8070  rankr1bg  8242  rankr1c  8260  carden2a  8368  dfac8clem  8434  dfac5lem4  8528  pwsdompw  8605  cfsuc  8658  cflim2  8664  enfin2i  8722  isf34lem4  8778  axdc4lem  8856  zornn0g  8906  uniimadomf  8941  fpwwe2lem8  9036  fpwwe2lem12  9040  fpwwe2lem13  9041  pwfseqlem1  9057  pwfseqlem5  9062  intgru  9213  addclpi  9291  addnidpi  9300  ltsonq  9368  nqpr  9413  reclem3pr  9448  recexsr  9505  supsrlem  9509  infmrcl  10547  nnnn0addcl  10851  un0addcl  10854  un0mulcl  10855  nn0nndivcl  10888  nn0ge0div  10957  uzind3  10981  uzind3OLD  10983  uzind4  11168  zsupss  11200  rpnnen1lem1  11237  rpnnen1lem2  11238  rpnnen1lem3  11239  rpnnen1lem5  11241  ltsubrp  11280  ltaddrp  11281  xrlttr  11375  qbtwnxr  11428  xltnegi  11444  xaddnemnf  11462  xaddnepnf  11463  xaddcom  11466  xnegdi  11469  xsubge0  11482  xrub  11532  fzind2  11924  seqof  12164  expp1  12173  expneg  12174  expcllem  12177  mulexpz  12206  expaddz  12210  expmulz  12212  faclbnd4lem3  12373  faclbnd4  12375  brfi1uzind  12532  swrd00  12645  swrd0  12658  cats1un  12701  reuccats1  12706  cshw0  12765  cshwn  12768  wwlktovfo  12896  shftf  12912  sqrtdiv  13099  leabs  13132  mulcn2  13418  summolem2  13538  fsumrev2  13597  geomulcvg  13685  prodmolem2  13742  zprod  13744  prodsn  13767  ruclem6  13968  dvdseq  14033  dvdsfac  14041  gcdcllem1  14149  rpexp1i  14262  hashdvds  14305  iserodd  14359  pcqcl  14380  pcid  14396  ismred  14999  funcpropd  15269  natpropd  15345  lubun  15753  odupos  15765  issubmd  15980  grpinvnzcl  16110  mulgneg  16160  mulgnn0z  16162  symgfixf1  16462  symgsssg  16492  symgfisg  16493  pgpssslw  16634  sylow2alem2  16638  sylow2a  16639  oddvdssubg  16861  gsumzunsnd  16982  gsumunsnfd  16983  gsum2dlem1  16997  gsum2dlem2  16998  gsum2dOLD  17000  ablfac1eu  17124  pgpfac1lem5  17130  gsumdixpOLD  17257  gsumdixp  17258  dvdsrcl2  17299  isdrngd  17421  evlslem4OLD  18173  evlslem4  18174  coe1tmmul2  18317  cnsubrg  18478  psgnodpm  18624  gsumcom3  18901  mpt2matmul  18948  cpmidpmat  19374  intcld  19541  neiptopnei  19633  ordtrest2lem  19704  lmss  19799  cmpcovf  19891  cncmp  19892  fincmp  19893  cmpsublem  19899  cmpsub  19900  uncon  19930  1stcfb  19946  2ndcsep  19960  refun0  20016  locfincmp  20027  1stckgenlem  20054  ptbasin  20078  ptbasfi  20082  ptunimpt  20096  ptuniconst  20099  dfac14  20119  ptcnp  20123  xkoptsub  20155  xkococnlem  20160  xkoinjcn  20188  qtopcmplem  20208  qtophmeo  20318  fbfinnfr  20342  isufil2  20409  isfcls  20510  xmetrtri  20858  xmetrtri2  20859  blssioo  21300  divcn  21372  bndth  21458  resscdrg  21798  minveclem3  21844  finiunmbl  21954  opnmbllem  22010  ismbf2d  22048  itg2seq  22149  ellimc2  22281  limcmpt2  22288  limcres  22290  dvlem  22300  dvidlem  22319  dvrec  22358  dveflem  22380  dvlip  22394  coe1mul3  22500  dvtaylp  22765  leibpilem2  23272  leibpi  23273  wilthlem2  23343  basellem3  23356  dvdsflip  23458  dchreq  23533  dchrsum  23544  lgsval3  23589  lgsdir2lem4  23601  2sqlem6  23644  rpvmasumlem  23672  dchrisum0fno1  23696  rpvmasum2  23697  pntrsumbnd2  23752  ostthlem1  23812  colmid  24065  lmiisolem  24161  axcontlem2  24268  axcontlem7  24273  umgraex  24323  usgraidx2vlem1  24391  nbgraf1olem3  24443  nbgraf1olem5  24445  cusconngra  24676  wlknwwlknfun  24710  wlknwwlkninj  24711  wlknwwlknsur  24712  wlkiswwlkfun  24717  wlkiswwlkinj  24718  wlkiswwlksur  24719  wwlkextfun  24729  wwlkextsur  24731  wlkv0  24760  clwwlkf  24794  grpoidinvlem3  25208  ablo32  25288  ablomuldiv  25291  ablodivdiv  25292  ablodiv32  25294  nvadd12  25516  nvscom  25524  nvsubsub23  25557  dipassr  25761  htthlem  25834  hsn0elch  26166  shscli  26235  nmopun  26933  branmfn  27024  mdslj1i  27238  mdslj2i  27239  atss  27265  chcv1  27274  dmdbr5ati  27341  fcnvgreu  27514  isoun  27520  ordtrest2NEWlem  27904  esumsplit  28063  esumpcvgval  28084  sigaclcu2  28120  volmeas  28203  mbfmco2  28236  oddpwdc  28293  eulerpartlemgvv  28315  ballotlemfc0  28431  ballotlemfcc  28432  subfacp1lem4  28627  erdszelem7  28641  erdszelem8  28642  erdsze2lem2  28648  rescon  28691  cvmsdisj  28715  cvmscld  28718  mclsax  28929  climuzcnv  29037  pocnv  29193  trpredmintr  29314  cgrid2  29653  btwncom  29664  btwnswapid2  29668  colinearperm1  29712  colinearperm3  29713  colinearperm2  29714  colinearperm4  29715  lineext  29726  colinbtwnle  29768  broutsideof2  29772  outsideofcom  29778  linecom  29800  linerflx2  29801  lineintmo  29807  bpolydiflem  29816  bpoly2  29819  bpoly3  29820  hfext  29840  fin2solem  30039  opnmbllem0  30050  mblfinlem3  30053  mbfposadd  30062  itg2addnclem3  30068  bddiblnc  30085  ftc1anclem6  30095  ftc1anc  30098  ntruni  30145  clsint2  30147  neibastop1  30177  eqfnun  30212  ac6gf  30223  heibor1lem  30305  isdrngo2  30361  unichnidl  30428  isfldidl  30465  cnf1dd  30490  ismrcd1  30630  isnacs3  30642  pellfundglb  30821  jm2.22  30937  jm2.23  30938  isnumbasgrplem1  31050  hbtlem6  31078  rngunsnply  31122  hashgcdlem  31157  phisum  31159  dvgrat  31193  cvgdvgrat  31194  lcmgcdlem  31212  nznngen  31221  uzmptshftfval  31251  iccshift  31558  iooshift  31562  prodsnf  31587  itgperiod  31780  fourierdlem42  31931  fourierdlem68  31957  fourierdlem93  31982  usgedgppr  32398  usgpredgv  32399  usgpredgvALT  32400  edgssv2ALT  32401  edgssv2  32402  usgedgvadf1lem1  32413  usgedgvadf1ALTlem1  32416  rabsubmgmd  32479  2zlidl  32740  lspsslco  33038  bnj521  33792  bnj1109  33845  bnj1294  33876  bnj545  33953  bnj605  33965  bnj594  33970  bnj934  33993  bnj953  33997  bnj1137  34051  bnj1174  34059  bnj1388  34089  bj-snsetex  34521  lkrss2N  34894  elpadd0  35533  ltrnu  35845  tendoex  36701  cdlemm10N  36845  dicfnN  36910  dihmeetlem2N  37026  dihlatat  37064  lcfrlem9  37277
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
  Copyright terms: Public domain W3C validator