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

Theorem sylan2b 491
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 206 . 2 (𝜑𝜒)
3 sylan2b.2 . 2 ((𝜓𝜒) → 𝜃)
42, 3sylan2 490 1 ((𝜓𝜑) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383
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 197  df-an 385
This theorem is referenced by:  syl2anb  495  eupickb  2567  eqtr3  2672  elnelne1  2936  elnelne2  2937  morex  3423  psssstr  3746  reuss2  3940  reupick  3944  reximdva0  3966  falseral0  4114  rabsneu  4296  opabss  4747  triun  4799  poirr  5075  wefrc  5137  xpcan  5605  fnfco  6107  fnressn  6465  fvtp3  6503  fvtp3g  6506  f1mpt  6558  offval  6946  ordsucuniel  7066  onzsl  7088  soex  7151  fun11iun  7168  dfoprab3  7268  1stconst  7310  2ndconst  7311  poxp  7334  fnwelem  7337  suppssr  7371  suppsssn  7375  oeordsuc  7719  oelim2  7720  omsmolem  7778  ssnnfi  8220  fiint  8278  unifi  8296  indexfi  8315  iinfi  8364  unwdomg  8530  inf3lem5  8567  rankr1bg  8704  rankr1c  8722  carden2a  8830  dfac8clem  8893  dfac5lem4  8987  pwsdompw  9064  cfsuc  9117  cflim2  9123  enfin2i  9181  isf34lem4  9237  axdc4lem  9315  zornn0g  9365  uniimadomf  9405  fpwwe2lem8  9497  fpwwe2lem12  9501  fpwwe2lem13  9502  pwfseqlem1  9518  pwfseqlem5  9523  intgru  9674  addclpi  9752  addnidpi  9761  ltsonq  9829  nqpr  9874  reclem3pr  9909  recexsr  9966  supsrlem  9970  nnnn0addcl  11361  un0addcl  11364  un0mulcl  11365  nn0nndivcl  11400  nn0ge0div  11484  uzind3  11509  uzind4  11784  zsupss  11815  rpnnen1lem2  11852  rpnnen1lem1  11853  rpnnen1lem3  11854  rpnnen1lem5  11856  rpnnen1lem1OLD  11859  rpnnen1lem3OLD  11860  rpnnen1lem5OLD  11862  ltsubrp  11904  ltaddrp  11905  xrlttr  12011  qbtwnxr  12069  xltnegi  12085  xaddnemnf  12105  xaddnepnf  12106  xaddcom  12109  xnegdi  12116  xsubge0  12129  xrub  12180  fzind2  12626  seqof  12898  expp1  12907  expneg  12908  expcllem  12911  mulexpz  12940  expaddz  12944  expmulz  12946  faclbnd4lem3  13122  faclbnd4  13124  fi1uzind  13317  swrd00  13463  swrd0  13480  cats1un  13521  reuccats1  13526  cshw0  13586  cshwn  13589  wwlktovfo  13747  shftf  13863  sqrtdiv  14050  leabs  14083  mulcn2  14370  summolem2  14491  fsumrev2  14558  geomulcvg  14651  prodmolem2  14709  zprod  14711  prodsn  14736  prodsnf  14738  bpolydiflem  14829  bpoly2  14832  bpoly3  14833  ruclem6  15008  dvdsflip  15086  dvdsfac  15095  gcdcllem1  15268  lcmgcdlem  15366  rpexp1i  15480  hashdvds  15527  hashgcdlem  15540  phisum  15542  iserodd  15587  pcqcl  15608  pcid  15624  ismred  16309  funcpropd  16607  natpropd  16683  lubun  17170  odupos  17182  issubmd  17396  grpinvnzcl  17534  mulgneg  17607  mulgnn0z  17614  symgfixf1  17903  symgsssg  17933  symgfisg  17934  pgpssslw  18075  sylow2alem2  18079  sylow2a  18080  oddvdssubg  18304  gsumzunsnd  18401  gsumunsnfd  18402  gsum2dlem1  18415  gsum2dlem2  18416  ablfac1eu  18518  pgpfac1lem5  18524  gsumdixp  18655  dvdsrcl2  18696  isdrngd  18820  evlslem4  19556  coe1tmmul2  19694  cnsubrg  19854  psgnodpm  19982  gsumcom3  20253  mpt2matmul  20300  cpmidpmat  20726  intcld  20892  neiptopnei  20984  ordtrest2lem  21055  lmss  21150  cmpcovf  21242  cncmp  21243  fincmp  21244  cmpsublem  21250  cmpsub  21251  unconn  21280  1stcfb  21296  2ndcsep  21310  refun0  21366  locfincmp  21377  1stckgenlem  21404  ptbasin  21428  ptbasfi  21432  ptunimpt  21446  ptuniconst  21449  dfac14  21469  ptcnp  21473  xkoptsub  21505  xkococnlem  21510  xkoinjcn  21538  qtopcmplem  21558  qtophmeo  21668  fbfinnfr  21692  isufil2  21759  isfcls  21860  xmetrtri  22207  xmetrtri2  22208  blssioo  22645  divcn  22718  bndth  22804  clmvscom  22936  resscdrg  23200  minveclem3  23246  finiunmbl  23358  opnmbllem  23415  ismbf2d  23453  itg2seq  23554  ellimc2  23686  limcmpt2  23693  limcres  23695  dvlem  23705  dvidlem  23724  dvrec  23763  dveflem  23787  dvlip  23801  coe1mul3  23904  dvtaylp  24169  leibpilem2  24713  leibpi  24714  wilthlem2  24840  basellem3  24854  dchreq  25028  dchrsum  25039  lgsval3  25085  lgsdir2lem4  25098  2sqlem6  25193  rpvmasumlem  25221  dchrisum0fno1  25245  rpvmasum2  25246  pntrsumbnd2  25301  ostthlem1  25361  colmid  25628  lmiisolem  25733  dfcgra2  25766  axcontlem2  25890  axcontlem7  25895  upgrex  26032  umgredg  26078  umgrpredgv  26080  umgredgne  26085  umgredgnlp  26087  usgredgppr  26133  edgssv2  26135  uspgredg2vlem  26160  usgredg2vlem1  26162  upgrres1  26250  nbuhgr2vtx1edgblem  26292  nbusgrf1o0  26315  hashnbusgrnn0  26322  iscplgredg  26369  uhgrvd00  26486  finsumvtxdg2size  26502  wlkepvtx  26612  wlknewwlksn  26841  wlknwwlksnfun  26842  wlknwwlksninj  26843  wlknwwlksnsur  26844  wlkwwlkfun  26849  wlkwwlkinj  26850  wlkwwlksur  26851  wwlksnextfun  26861  wwlksnextsur  26863  elwwlks2ons3im  26919  elwwlks2ons3OLD  26921  wwlks2onsym  26924  clwwlkf  27010  fusgreghash2wspv  27315  numclwwlk5lem  27374  grpoidinvlem3  27488  ablo32  27531  ablomuldiv  27534  ablodivdiv  27535  ablodiv32  27537  nvscom  27612  dipassr  27829  htthlem  27902  hsn0elch  28233  shscli  28304  nmopun  29001  branmfn  29092  mdslj1i  29306  mdslj2i  29307  atss  29333  chcv1  29342  dmdbr5ati  29409  fcnvgreu  29600  isoun  29607  prodpr  29700  prodtp  29701  ordtrest2NEWlem  30096  esumsplit  30243  esumpad2  30246  esumpcvgval  30268  sigaclcu2  30311  ldgenpisyslem1  30354  volmeas  30422  mbfmco2  30455  omsmeas  30513  oddpwdc  30544  eulerpartlemgvv  30566  ballotlemfc0  30682  ballotlemfcc  30683  prodfzo03  30809  circlemethhgt  30849  bnj521  30931  bnj1109  30983  bnj1294  31014  bnj545  31091  bnj605  31103  bnj594  31108  bnj934  31131  bnj953  31135  bnj1137  31189  bnj1174  31197  bnj1388  31227  subfacp1lem4  31291  erdszelem7  31305  erdszelem8  31306  erdsze2lem2  31312  resconn  31354  cvmsdisj  31378  cvmscld  31381  mclsax  31592  climuzcnv  31691  pocnv  31779  trpredmintr  31855  nosupno  31974  cgrid2  32235  btwncom  32246  btwnswapid2  32250  colinearperm1  32294  colinearperm3  32295  colinearperm2  32296  colinearperm4  32297  lineext  32308  colinbtwnle  32350  broutsideof2  32354  outsideofcom  32360  linecom  32382  linerflx2  32383  lineintmo  32389  fwddifn0  32396  hfext  32415  ntruni  32447  clsint2  32449  neibastop1  32479  bj-snsetex  33076  relowlssretop  33341  fin2solem  33525  matunitlindflem1  33535  poimirlem4  33543  poimirlem25  33564  poimirlem32  33571  opnmbllem0  33575  mblfinlem3  33578  mbfposadd  33587  itg2addnclem3  33593  bddiblnc  33610  ftc1anclem6  33620  ftc1anc  33623  eqfnun  33646  ac6gf  33657  heibor1lem  33738  isdrngo2  33887  unichnidl  33960  isfldidl  33997  cnf1dd  34022  lkrss2N  34774  elpadd0  35413  ltrnu  35725  tendoex  36580  cdlemm10N  36724  dicfnN  36789  dihmeetlem2N  36905  dihlatat  36943  lcfrlem9  37156  ismrcd1  37578  isnacs3  37590  pellfundglb  37766  jm2.22  37879  jm2.23  37880  isnumbasgrplem1  37988  hbtlem6  38016  rngunsnply  38060  dvgrat  38828  cvgdvgrat  38829  nznngen  38832  uzmptshftfval  38862  iccshift  40062  iooshift  40066  xlimbr  40371  itgperiod  40515  fourierdlem42  40684  fourierdlem68  40709  fourierdlem93  40734  elprneb  41620  rabsubmgmd  42116  2zlidl  42259  lspsslco  42551  setrec2lem2  42766
  Copyright terms: Public domain W3C validator