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

Theorem sylan2b 593
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 217 . 2 (𝜑𝜒)
3 sylan2b.2 . 2 ((𝜓𝜒) → 𝜃)
42, 3sylan2 592 1 ((𝜓𝜑) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396
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 208  df-an 397
This theorem is referenced by:  syl2anb  597  eupickb  2716  2eu1  2731  2eu1v  2733  eqtr3  2843  elnelne1  3133  elnelne2  3134  morex  3709  psssstr  4082  reuss2  4282  reupick  4286  reximdva0  4311  falseral0  4457  rabsneu  4659  invdisjrabw  5043  opabss  5122  triun  5177  triin  5179  poirr  5479  wefrc  5543  xpcan  6027  fnfco  6537  fnressn  6913  fvtp3  6952  fvtp3g  6955  f1mpt  7010  offval  7405  ordsucuniel  7527  onzsl  7549  soex  7614  fiunlemw  7631  fiunw  7632  f1iunw  7633  fiunlem  7634  fiun  7635  f1iun  7636  dfoprab3  7743  poxp  7813  fnwelem  7816  suppssr  7852  suppsssn  7856  suppofssd  7858  oeordsuc  8210  oelim2  8211  omsmolem  8270  ssnnfi  8726  fiint  8784  unifi  8802  indexfi  8821  iinfi  8870  unwdomg  9037  inf3lem5  9084  rankr1bg  9221  rankr1c  9239  carden2a  9384  dfac8clem  9447  dfac5lem4  9541  pwsdompw  9615  cfsuc  9668  cflim2  9674  enfin2i  9732  isf34lem4  9788  axdc4lem  9866  zornn0g  9916  uniimadomf  9956  fpwwe2lem8  10048  fpwwe2lem12  10052  fpwwe2lem13  10053  pwfseqlem1  10069  pwfseqlem5  10074  intgru  10225  addclpi  10303  addnidpi  10312  ltsonq  10380  nqpr  10425  reclem3pr  10460  recexsr  10518  supsrlem  10522  nnnn0addcl  11916  un0addcl  11919  un0mulcl  11920  nn0nndivcl  11955  nn0ge0div  12040  uzind3  12065  uzind4  12295  zsupss  12326  rpnnen1lem2  12366  rpnnen1lem1  12367  rpnnen1lem3  12368  rpnnen1lem5  12370  ltsubrp  12415  ltaddrp  12416  xrlttr  12523  qbtwnxr  12583  xltnegi  12599  xaddnemnf  12619  xaddnepnf  12620  xaddcom  12623  xnegdi  12631  xsubge0  12644  xrub  12695  fzind2  13145  seqof  13417  expp1  13426  expneg  13427  expcllem  13430  mulexpz  13459  expaddz  13463  expmulz  13465  faclbnd4lem3  13645  faclbnd4  13647  fi1uzind  13845  swrd00  13996  swrd0  14010  cats1un  14073  reuccatpfxs1  14099  cshw0  14146  cshwn  14149  wwlktovfo  14312  shftf  14428  sqrtdiv  14615  leabs  14649  mulcn2  14942  summolem2  15063  fsumrev2  15127  geomulcvg  15222  prodmolem2  15279  zprod  15281  prodsn  15306  prodsnf  15308  fprodle  15340  bpolydiflem  15398  bpoly2  15401  bpoly3  15402  ruclem6  15578  dvdsflip  15657  dvdsfac  15666  gcdcllem1  15838  lcmgcdlem  15940  rpexp1i  16055  hashdvds  16102  hashgcdlem  16115  phisum  16117  iserodd  16162  pcqcl  16183  pcid  16199  ismred  16863  funcpropd  17160  natpropd  17236  lubun  17723  odupos  17735  sgrpidmnd  17906  issubmd  17961  grpinvnzcl  18111  mulgneg  18186  mulgnn0z  18194  symgfixf1  18496  symgsssg  18526  symgfisg  18527  pgpssslw  18670  sylow2alem2  18674  sylow2a  18675  oddvdssubg  18906  gsumzunsnd  19007  gsumunsnfd  19008  gsum2dlem1  19021  gsum2dlem2  19022  gsumcom3  19029  ablfac1eu  19126  pgpfac1lem5  19132  gsumdixp  19290  dvdsrcl2  19331  isdrngd  19458  evlslem4  20218  coe1tmmul2  20374  cnsubrg  20535  psgnodpm  20662  mpomatmul  20985  cpmidpmat  21411  intcld  21578  neiptopnei  21670  ordtrest2lem  21741  lmss  21836  cmpcovf  21929  cncmp  21930  fincmp  21931  cmpsublem  21937  cmpsub  21938  unconn  21967  1stcfb  21983  2ndcsep  21997  refun0  22053  locfincmp  22064  1stckgenlem  22091  ptbasin  22115  ptbasfi  22119  ptunimpt  22133  ptuniconst  22136  dfac14  22156  ptcnp  22160  xkoptsub  22192  xkococnlem  22197  xkoinjcn  22225  qtopcmplem  22245  qtophmeo  22355  fbfinnfr  22379  isufil2  22446  isfcls  22547  xmetrtri  22894  xmetrtri2  22895  blssioo  23332  divcn  23405  bndth  23491  clmvscom  23623  resscdrg  23890  minveclem3  23961  finiunmbl  24074  opnmbllem  24131  ismbf2d  24170  itg2seq  24272  ellimc2  24404  limcmpt2  24411  limcres  24413  dvlem  24423  dvidlem  24442  dvrec  24481  dveflem  24505  dvlip  24519  coe1mul3  24622  dvtaylp  24887  leibpilem2  25447  leibpi  25448  wilthlem2  25574  basellem3  25588  dchreq  25762  dchrsum  25773  lgsval3  25819  lgsdir2lem4  25832  2sqlem6  25927  rpvmasumlem  25991  dchrisum0fno1  26015  rpvmasum2  26016  pntrsumbnd2  26071  ostthlem1  26131  colmid  26402  lmiisolem  26510  dfcgra2  26544  axcontlem2  26679  axcontlem7  26684  upgrex  26805  umgredg  26851  umgrpredgv  26853  umgredgne  26858  umgredgnlp  26860  usgredgppr  26906  edgssv2  26908  uspgredg2vlem  26933  usgredg2vlem1  26935  upgrres1  27023  nbuhgr2vtx1edgblem  27061  nbusgrf1o0  27079  hashnbusgrnn0  27086  iscplgredg  27127  uhgrvd00  27244  finsumvtxdg2size  27260  wlkepvtx  27370  wlknewwlksn  27593  wwlksnextfun  27604  wwlksnextsurj  27606  elwwlks2ons3im  27661  wwlks2onsym  27665  clwwlkf  27754  fusgreghash2wspv  28042  numclwwlk5lem  28094  grpoidinvlem3  28211  ablo32  28254  ablomuldiv  28257  ablodivdiv  28258  ablodiv32  28260  nvscom  28334  dipassr  28551  htthlem  28622  hsn0elch  28953  shscli  29022  nmopun  29719  branmfn  29810  mdslj1i  30024  mdslj2i  30025  atss  30051  chcv1  30060  dmdbr5ati  30127  fnpreimac  30345  fcnvgreu  30347  isoun  30364  fsuppcurry1  30388  fsuppcurry2  30389  fzne1  30438  prodpr  30470  prodtp  30471  pmtrprfv2  30660  isprmidlc  30882  ordtrest2NEWlem  31065  esumsplit  31212  esumpad2  31215  esumpcvgval  31237  sigaclcu2  31279  ldgenpisyslem1  31322  volmeas  31390  mbfmco2  31423  omsmeas  31481  oddpwdc  31512  eulerpartlemgvv  31534  ballotlemfc0  31650  ballotlemfcc  31651  prodfzo03  31774  circlemethhgt  31814  bnj521  31907  bnj1109  31958  bnj1294  31989  bnj545  32067  bnj605  32079  bnj594  32084  bnj934  32107  bnj953  32111  bnj1137  32165  bnj1174  32173  bnj1388  32203  subfacp1lem4  32328  erdszelem7  32342  erdszelem8  32343  erdsze2lem2  32349  resconn  32391  cvmsdisj  32415  cvmscld  32418  satf0op  32522  mclsax  32714  climuzcnv  32812  pocnv  32897  trpredmintr  32968  fprlem2  33036  nosupno  33101  cgrid2  33362  btwncom  33373  btwnswapid2  33377  colinearperm1  33421  colinearperm3  33422  colinearperm2  33423  colinearperm4  33424  lineext  33435  colinbtwnle  33477  broutsideof2  33481  outsideofcom  33487  linecom  33509  linerflx2  33510  lineintmo  33516  fwddifn0  33523  hfext  33542  ntruni  33573  clsint2  33575  neibastop1  33605  bj-snsetex  34173  relowlssretop  34527  pibt2  34581  fin2solem  34760  lindsadd  34767  matunitlindflem1  34770  poimirlem4  34778  poimirlem25  34799  poimirlem32  34806  opnmbllem0  34810  mblfinlem3  34813  mbfposadd  34821  itg2addnclem3  34827  bddiblnc  34844  ftc1anclem6  34854  ftc1anc  34857  eqfnun  34880  ac6gf  34890  heibor1lem  34970  isdrngo2  35119  unichnidl  35192  isfldidl  35229  cnf1dd  35251  lkrss2N  36187  elpadd0  36827  ltrnu  37139  tendoex  37993  cdlemm10N  38136  dicfnN  38201  dihmeetlem2N  38317  dihlatat  38355  lcfrlem9  38568  ismrcd1  39175  isnacs3  39187  pellfundglb  39362  jm2.22  39472  jm2.23  39473  isnumbasgrplem1  39581  hbtlem6  39609  rngunsnply  39653  dvgrat  40524  cvgdvgrat  40525  nznngen  40528  uzmptshftfval  40558  rnmptlb  41394  rnmptbddlem  41395  rnmptbd2lem  41400  iccshift  41674  iooshift  41678  liminflbuz2  41976  xlimbr  41988  itgperiod  42146  fourierdlem42  42315  fourierdlem68  42340  fourierdlem93  42365  elprneb  43145  dfatcolem  43335  ichnfb  43472  prproropf1olem1  43512  prproropf1olem3  43514  rabsubmgmd  43905  2zlidl  44103  lspsslco  44390
  Copyright terms: Public domain W3C validator