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

Theorem sylan2b 490
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 204 . 2 (𝜑𝜒)
3 sylan2b.2 . 2 ((𝜓𝜒) → 𝜃)
42, 3sylan2 489 1 ((𝜓𝜑) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wa 382
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 195  df-an 384
This theorem is referenced by:  syl2anb  494  eupickb  2525  eqtr3  2630  elnelne1  2892  elnelne2  2893  morex  3356  psssstr  3674  reuss2  3865  reupick  3869  reximdva0  3890  rabsneu  4207  opabss  4640  triun  4688  poirr  4959  wefrc  5021  xpcan  5474  fnfco  5966  fnressn  6307  fvtp3  6344  fvtp3g  6347  f1mpt  6396  offval  6779  ordsucuniel  6893  onzsl  6915  soex  6979  fun11iun  6996  dfoprab3  7092  1stconst  7129  2ndconst  7130  poxp  7153  fnwelem  7156  suppssr  7190  suppsssn  7194  oeordsuc  7538  oelim2  7539  omsmolem  7597  ssnnfi  8041  fiint  8099  unifi  8115  indexfi  8134  iinfi  8183  unwdomg  8349  inf3lem5  8389  rankr1bg  8526  rankr1c  8544  carden2a  8652  dfac8clem  8715  dfac5lem4  8809  pwsdompw  8886  cfsuc  8939  cflim2  8945  enfin2i  9003  isf34lem4  9059  axdc4lem  9137  zornn0g  9187  uniimadomf  9223  fpwwe2lem8  9315  fpwwe2lem12  9319  fpwwe2lem13  9320  pwfseqlem1  9336  pwfseqlem5  9341  intgru  9492  addclpi  9570  addnidpi  9579  ltsonq  9647  nqpr  9692  reclem3pr  9727  recexsr  9784  supsrlem  9788  nnnn0addcl  11172  un0addcl  11175  un0mulcl  11176  nn0nndivcl  11211  nn0ge0div  11280  uzind3  11305  uzind4  11580  zsupss  11611  rpnnen1lem2  11648  rpnnen1lem1  11649  rpnnen1lem3  11650  rpnnen1lem5  11652  rpnnen1lem1OLD  11655  rpnnen1lem3OLD  11656  rpnnen1lem5OLD  11658  ltsubrp  11700  ltaddrp  11701  xrlttr  11810  qbtwnxr  11866  xltnegi  11882  xaddnemnf  11901  xaddnepnf  11902  xaddcom  11905  xnegdi  11909  xsubge0  11922  xrub  11972  fzind2  12405  seqof  12677  expp1  12686  expneg  12687  expcllem  12690  mulexpz  12719  expaddz  12723  expmulz  12725  faclbnd4lem3  12901  faclbnd4  12903  fi1uzind  13082  fi1uzindOLD  13088  swrd00  13218  swrd0  13234  cats1un  13275  reuccats1  13280  cshw0  13339  cshwn  13342  wwlktovfo  13497  shftf  13615  sqrtdiv  13802  leabs  13835  mulcn2  14122  summolem2  14242  fsumrev2  14304  geomulcvg  14394  prodmolem2  14452  zprod  14454  prodsn  14479  prodsnf  14481  bpolydiflem  14572  bpoly2  14575  bpoly3  14576  ruclem6  14751  dvdsflip  14825  dvdsfac  14834  gcdcllem1  15007  lcmgcdlem  15105  rpexp1i  15219  hashdvds  15266  hashgcdlem  15279  phisum  15281  iserodd  15326  pcqcl  15347  pcid  15363  ismred  16033  funcpropd  16331  natpropd  16407  lubun  16894  odupos  16906  issubmd  17120  grpinvnzcl  17258  mulgneg  17331  mulgnn0z  17338  symgfixf1  17628  symgsssg  17658  symgfisg  17659  pgpssslw  17800  sylow2alem2  17804  sylow2a  17805  oddvdssubg  18029  gsumzunsnd  18126  gsumunsnfd  18127  gsum2dlem1  18140  gsum2dlem2  18141  ablfac1eu  18243  pgpfac1lem5  18249  gsumdixp  18380  dvdsrcl2  18421  isdrngd  18543  evlslem4  19277  coe1tmmul2  19415  cnsubrg  19573  psgnodpm  19700  gsumcom3  19971  mpt2matmul  20018  cpmidpmat  20444  intcld  20601  neiptopnei  20693  ordtrest2lem  20764  lmss  20859  cmpcovf  20951  cncmp  20952  fincmp  20953  cmpsublem  20959  cmpsub  20960  uncon  20989  1stcfb  21005  2ndcsep  21019  refun0  21075  locfincmp  21086  1stckgenlem  21113  ptbasin  21137  ptbasfi  21141  ptunimpt  21155  ptuniconst  21158  dfac14  21178  ptcnp  21182  xkoptsub  21214  xkococnlem  21219  xkoinjcn  21247  qtopcmplem  21267  qtophmeo  21377  fbfinnfr  21402  isufil2  21469  isfcls  21570  xmetrtri  21917  xmetrtri2  21918  blssioo  22353  divcn  22426  bndth  22512  clmvscom  22645  resscdrg  22906  minveclem3  22952  finiunmbl  23063  opnmbllem  23119  ismbf2d  23158  itg2seq  23259  ellimc2  23391  limcmpt2  23398  limcres  23400  dvlem  23410  dvidlem  23429  dvrec  23468  dveflem  23490  dvlip  23504  coe1mul3  23607  dvtaylp  23872  leibpilem2  24412  leibpi  24413  wilthlem2  24539  basellem3  24553  dchreq  24727  dchrsum  24738  lgsval3  24784  lgsdir2lem4  24797  2sqlem6  24892  rpvmasumlem  24920  dchrisum0fno1  24944  rpvmasum2  24945  pntrsumbnd2  25000  ostthlem1  25060  colmid  25328  lmiisolem  25433  dfcgra2  25466  axcontlem2  25590  axcontlem7  25595  umgraex  25645  usgraidx2vlem1  25713  nbgraf1olem3  25765  nbgraf1olem5  25767  cusconngra  25997  wlknwwlknfun  26031  wlknwwlkninj  26032  wlknwwlknsur  26033  wlkiswwlkfun  26038  wlkiswwlkinj  26039  wlkiswwlksur  26040  wwlkextfun  26050  wwlkextsur  26052  wlkv0  26081  clwwlkf  26115  grpoidinvlem3  26537  ablo32  26580  ablomuldiv  26583  ablodivdiv  26584  ablodiv32  26586  nvscom  26661  dipassr  26878  htthlem  26951  hsn0elch  27282  shscli  27353  nmopun  28050  branmfn  28141  mdslj1i  28355  mdslj2i  28356  atss  28382  chcv1  28391  dmdbr5ati  28458  fcnvgreu  28648  isoun  28655  ordtrest2NEWlem  29089  esumsplit  29235  esumpad2  29238  esumpcvgval  29260  sigaclcu2  29303  ldgenpisyslem1  29346  volmeas  29414  mbfmco2  29447  omsmeas  29505  oddpwdc  29536  eulerpartlemgvv  29558  ballotlemfc0  29674  ballotlemfcc  29675  bnj521  29852  bnj1109  29904  bnj1294  29935  bnj545  30012  bnj605  30024  bnj594  30029  bnj934  30052  bnj953  30056  bnj1137  30110  bnj1174  30118  bnj1388  30148  subfacp1lem4  30212  erdszelem7  30226  erdszelem8  30227  erdsze2lem2  30233  rescon  30275  cvmsdisj  30299  cvmscld  30302  mclsax  30513  climuzcnv  30612  pocnv  30700  trpredmintr  30768  cgrid2  31073  btwncom  31084  btwnswapid2  31088  colinearperm1  31132  colinearperm3  31133  colinearperm2  31134  colinearperm4  31135  lineext  31146  colinbtwnle  31188  broutsideof2  31192  outsideofcom  31198  linecom  31220  linerflx2  31221  lineintmo  31227  fwddifn0  31234  hfext  31253  ntruni  31285  clsint2  31287  neibastop1  31317  bj-snsetex  31927  relowlssretop  32170  fin2solem  32348  matunitlindflem1  32358  poimirlem4  32366  poimirlem25  32387  poimirlem32  32394  opnmbllem0  32398  mblfinlem3  32401  mbfposadd  32410  itg2addnclem3  32416  bddiblnc  32433  ftc1anclem6  32443  ftc1anc  32446  eqfnun  32469  ac6gf  32480  heibor1lem  32561  isdrngo2  32710  unichnidl  32783  isfldidl  32820  cnf1dd  32845  lkrss2N  33257  elpadd0  33896  ltrnu  34208  tendoex  35064  cdlemm10N  35208  dicfnN  35273  dihmeetlem2N  35389  dihlatat  35427  lcfrlem9  35640  ismrcd1  36062  isnacs3  36074  pellfundglb  36250  jm2.22  36363  jm2.23  36364  isnumbasgrplem1  36473  hbtlem6  36501  rngunsnply  36545  dvgrat  37316  cvgdvgrat  37317  nznngen  37320  uzmptshftfval  37350  iccshift  38374  iooshift  38378  itgperiod  38656  fourierdlem42  38825  fourierdlem68  38850  fourierdlem93  38875  elprneb  39723  falseral0  40092  upgrex  40299  umgredg  40352  umgrpredgav  40353  umgredgne  40356  umgredgnlp  40358  usgredgappr  40404  edgassv2  40406  uspgredg2vlem  40431  usgredg2vlem1  40433  upgrres1  40513  nbuhgr2vtx1edgblem  40554  nbusgrf1o0  40578  hashnbusgrnn0  40585  iscplgredg  40620  uhgrvd00  40731  1wlkepvtx  40849  wlknewwlksn  41065  wlknwwlksnfun  41066  wlknwwlksninj  41067  wlknwwlksnsur  41068  wlkwwlkfun  41073  wlkwwlkinj  41074  wlkwwlksur  41075  wwlksnextfun  41085  wwlksnextsur  41087  elwwlks2ons3  41140  clwwlksf  41203  fusgreghash2wspv  41480  rabsubmgmd  41562  2zlidl  41705  lspsslco  42001
  Copyright terms: Public domain W3C validator