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

Theorem sylan2b 587
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 207 . 2 (𝜑𝜒)
3 sylan2b.2 . 2 ((𝜓𝜒) → 𝜃)
42, 3sylan2 586 1 ((𝜓𝜑) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384
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 198  df-an 385
This theorem is referenced by:  syl2anb  591  eupickb  2660  eqtr3  2786  elnelne1  3050  elnelne2  3051  morex  3549  psssstr  3874  reuss2  4071  reupick  4075  reximdva0  4097  falseral0  4238  rabsneu  4419  opabss  4873  triun  4924  triin  4926  poirr  5209  wefrc  5271  xpcan  5753  fnfco  6251  fnressn  6617  fvtp3  6655  fvtp3g  6658  f1mpt  6710  offval  7102  ordsucuniel  7222  onzsl  7244  soex  7307  fun11iun  7324  dfoprab3  7424  poxp  7491  fnwelem  7494  suppssr  7529  suppsssn  7533  oeordsuc  7879  oelim2  7880  omsmolem  7938  ssnnfi  8386  fiint  8444  unifi  8462  indexfi  8481  iinfi  8530  unwdomg  8696  inf3lem5  8744  rankr1bg  8881  rankr1c  8899  carden2a  9043  dfac8clem  9106  dfac5lem4  9200  pwsdompw  9279  cfsuc  9332  cflim2  9338  enfin2i  9396  isf34lem4  9452  axdc4lem  9530  zornn0g  9580  uniimadomf  9620  fpwwe2lem8  9712  fpwwe2lem12  9716  fpwwe2lem13  9717  pwfseqlem1  9733  pwfseqlem5  9738  intgru  9889  addclpi  9967  addnidpi  9976  ltsonq  10044  nqpr  10089  reclem3pr  10124  recexsr  10181  supsrlem  10185  nnnn0addcl  11570  un0addcl  11573  un0mulcl  11574  nn0nndivcl  11609  nn0ge0div  11693  uzind3  11718  uzind4  11946  zsupss  11978  rpnnen1lem2  12015  rpnnen1lem1  12016  rpnnen1lem3  12017  rpnnen1lem5  12019  ltsubrp  12064  ltaddrp  12065  xrlttr  12173  qbtwnxr  12233  xltnegi  12249  xaddnemnf  12269  xaddnepnf  12270  xaddcom  12273  xnegdi  12280  xsubge0  12293  xrub  12344  fzind2  12794  seqof  13065  expp1  13074  expneg  13075  expcllem  13078  mulexpz  13107  expaddz  13111  expmulz  13113  faclbnd4lem3  13286  faclbnd4  13288  fi1uzind  13480  swrd00  13619  swrd0  13636  cats1un  13719  reuccats1OLD  13726  reuccatpfxs1  13761  cshw0  13823  cshwn  13826  wwlktovfo  13988  shftf  14104  sqrtdiv  14291  leabs  14324  mulcn2  14611  summolem2  14732  fsumrev2  14798  geomulcvg  14891  prodmolem2  14948  zprod  14950  prodsn  14975  prodsnf  14977  bpolydiflem  15067  bpoly2  15070  bpoly3  15071  ruclem6  15246  dvdsflip  15324  dvdsfac  15333  gcdcllem1  15502  lcmgcdlem  15600  rpexp1i  15712  hashdvds  15759  hashgcdlem  15772  phisum  15774  iserodd  15819  pcqcl  15840  pcid  15856  ismred  16528  funcpropd  16825  natpropd  16901  lubun  17389  odupos  17401  issubmd  17615  grpinvnzcl  17754  mulgneg  17826  mulgnn0z  17833  symgfixf1  18120  symgsssg  18150  symgfisg  18151  pgpssslw  18293  sylow2alem2  18297  sylow2a  18298  oddvdssubg  18524  gsumzunsnd  18621  gsumunsnfd  18622  gsum2dlem1  18635  gsum2dlem2  18636  ablfac1eu  18739  pgpfac1lem5  18745  gsumdixp  18876  dvdsrcl2  18917  isdrngd  19041  evlslem4  19781  coe1tmmul2  19919  cnsubrg  20079  psgnodpm  20206  gsumcom3  20481  mpt2matmul  20529  cpmidpmat  20957  intcld  21124  neiptopnei  21216  ordtrest2lem  21287  lmss  21382  cmpcovf  21474  cncmp  21475  fincmp  21476  cmpsublem  21482  cmpsub  21483  unconn  21512  1stcfb  21528  2ndcsep  21542  refun0  21598  locfincmp  21609  1stckgenlem  21636  ptbasin  21660  ptbasfi  21664  ptunimpt  21678  ptuniconst  21681  dfac14  21701  ptcnp  21705  xkoptsub  21737  xkococnlem  21742  xkoinjcn  21770  qtopcmplem  21790  qtophmeo  21900  fbfinnfr  21924  isufil2  21991  isfcls  22092  xmetrtri  22439  xmetrtri2  22440  blssioo  22877  divcn  22950  bndth  23036  clmvscom  23168  resscdrg  23435  minveclem3  23489  finiunmbl  23602  opnmbllem  23659  ismbf2d  23698  itg2seq  23800  ellimc2  23932  limcmpt2  23939  limcres  23941  dvlem  23951  dvidlem  23970  dvrec  24009  dveflem  24033  dvlip  24047  coe1mul3  24150  dvtaylp  24415  leibpilem2  24959  leibpi  24960  wilthlem2  25086  basellem3  25100  dchreq  25274  dchrsum  25285  lgsval3  25331  lgsdir2lem4  25344  2sqlem6  25439  rpvmasumlem  25467  dchrisum0fno1  25491  rpvmasum2  25492  pntrsumbnd2  25547  ostthlem1  25607  colmid  25874  lmiisolem  25979  dfcgra2  26012  axcontlem2  26136  axcontlem7  26141  upgrex  26264  umgredg  26311  umgrpredgv  26313  umgredgne  26318  umgredgnlp  26320  usgredgppr  26366  edgssv2  26368  uspgredg2vlem  26393  usgredg2vlem1  26395  upgrres1  26484  nbuhgr2vtx1edgblem  26526  nbusgrf1o0  26550  hashnbusgrnn0  26557  iscplgredg  26604  uhgrvd00  26721  finsumvtxdg2size  26737  wlkepvtx  26847  wlknewwlksn  27079  wlknwwlksnfunOLD  27080  wlknwwlksninjOLD  27081  wlknwwlksnsurOLD  27082  wlkwwlkfunOLD  27088  wlkwwlkinjOLD  27089  wlkwwlksurOLD  27090  wwlksnextfun  27104  wwlksnextsurj  27106  wwlksnextfunOLD  27109  wwlksnextsurOLD  27111  elwwlks2ons3im  27177  elwwlks2ons3OLD  27179  wwlks2onsym  27182  clwwlkfOLD  27290  clwwlkf  27295  fusgreghash2wspv  27615  numclwwlk5lem  27703  grpoidinvlem3  27817  ablo32  27860  ablomuldiv  27863  ablodivdiv  27864  ablodiv32  27866  nvscom  27940  dipassr  28157  htthlem  28230  hsn0elch  28561  shscli  28632  nmopun  29329  branmfn  29420  mdslj1i  29634  mdslj2i  29635  atss  29661  chcv1  29670  dmdbr5ati  29737  fcnvgreu  29921  isoun  29928  prodpr  30021  prodtp  30022  ordtrest2NEWlem  30415  esumsplit  30562  esumpad2  30565  esumpcvgval  30587  sigaclcu2  30630  ldgenpisyslem1  30673  volmeas  30741  mbfmco2  30774  omsmeas  30832  oddpwdc  30863  eulerpartlemgvv  30885  ballotlemfc0  31002  ballotlemfcc  31003  prodfzo03  31132  circlemethhgt  31172  bnj521  31254  bnj1109  31305  bnj1294  31336  bnj545  31413  bnj605  31425  bnj594  31430  bnj934  31453  bnj953  31457  bnj1137  31511  bnj1174  31519  bnj1388  31549  subfacp1lem4  31613  erdszelem7  31627  erdszelem8  31628  erdsze2lem2  31634  resconn  31676  cvmsdisj  31700  cvmscld  31703  mclsax  31914  climuzcnv  32011  pocnv  32098  trpredmintr  32174  nosupno  32293  cgrid2  32554  btwncom  32565  btwnswapid2  32569  colinearperm1  32613  colinearperm3  32614  colinearperm2  32615  colinearperm4  32616  lineext  32627  colinbtwnle  32669  broutsideof2  32673  outsideofcom  32679  linecom  32701  linerflx2  32702  lineintmo  32708  fwddifn0  32715  hfext  32734  ntruni  32765  clsint2  32767  neibastop1  32797  bj-snsetex  33378  relowlssretop  33644  fin2solem  33819  matunitlindflem1  33829  poimirlem4  33837  poimirlem25  33858  poimirlem32  33865  opnmbllem0  33869  mblfinlem3  33872  mbfposadd  33880  itg2addnclem3  33886  bddiblnc  33903  ftc1anclem6  33913  ftc1anc  33916  eqfnun  33939  ac6gf  33950  heibor1lem  34030  isdrngo2  34179  unichnidl  34252  isfldidl  34289  cnf1dd  34314  lkrss2N  35125  elpadd0  35765  ltrnu  36077  tendoex  36931  cdlemm10N  37074  dicfnN  37139  dihmeetlem2N  37255  dihlatat  37293  lcfrlem9  37506  ismrcd1  37939  isnacs3  37951  pellfundglb  38127  jm2.22  38239  jm2.23  38240  isnumbasgrplem1  38348  hbtlem6  38376  rngunsnply  38420  dvgrat  39185  cvgdvgrat  39186  nznngen  39189  uzmptshftfval  39219  iccshift  40383  iooshift  40387  xlimbr  40691  itgperiod  40834  fourierdlem42  41003  fourierdlem68  41028  fourierdlem93  41053  elprneb  41811  dfatcolem  42003  rabsubmgmd  42460  2zlidl  42603  lspsslco  42895
  Copyright terms: Public domain W3C validator