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

Theorem sylan2b 596
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 219 . 2 (𝜑𝜒)
3 sylan2b.2 . 2 ((𝜓𝜒) → 𝜃)
42, 3sylan2 595 1 ((𝜓𝜑) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399
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 210  df-an 400
This theorem is referenced by:  syl2anb  600  eupickb  2723  2eu1  2738  2eu1v  2739  eqtr3  2846  elnelne1  3128  elnelne2  3129  morex  3696  psssstr  4069  reuss2  4268  reupick  4272  reximdva0  4295  falseral0  4442  rabsneu  4650  invdisjrabw  5037  opabss  5116  triun  5171  triin  5173  poirr  5472  wefrc  5536  xpcan  6020  fnfco  6533  fnressn  6911  fvtp3  6950  fvtp3g  6953  f1mpt  7011  offval  7410  ordsucuniel  7533  onzsl  7555  soex  7621  fiunlem  7638  fiun  7639  f1iun  7640  dfoprab3  7747  poxp  7818  fnwelem  7821  suppssr  7857  suppsssn  7861  suppofssd  7863  oeordsuc  8216  oelim2  8217  omsmolem  8276  ssnnfi  8734  fiint  8792  unifi  8810  indexfi  8829  iinfi  8878  unwdomg  9045  inf3lem5  9092  rankr1bg  9229  rankr1c  9247  carden2a  9392  dfac8clem  9456  dfac5lem4  9550  pwsdompw  9624  cfsuc  9677  cflim2  9683  enfin2i  9741  isf34lem4  9797  axdc4lem  9875  zornn0g  9925  uniimadomf  9965  fpwwe2lem8  10057  fpwwe2lem12  10061  fpwwe2lem13  10062  pwfseqlem1  10078  pwfseqlem5  10083  intgru  10234  addclpi  10312  addnidpi  10321  ltsonq  10389  nqpr  10434  reclem3pr  10469  recexsr  10527  supsrlem  10531  nnnn0addcl  11924  un0addcl  11927  un0mulcl  11928  nn0nndivcl  11963  nn0ge0div  12048  uzind3  12073  uzind4  12303  zsupss  12334  rpnnen1lem2  12373  rpnnen1lem1  12374  rpnnen1lem3  12375  rpnnen1lem5  12377  ltsubrp  12422  ltaddrp  12423  xrlttr  12530  qbtwnxr  12590  xltnegi  12606  xaddnemnf  12626  xaddnepnf  12627  xaddcom  12630  xnegdi  12638  xsubge0  12651  xrub  12702  fzind2  13159  seqof  13432  expp1  13441  expneg  13442  expcllem  13445  mulexpz  13474  expaddz  13478  expmulz  13480  faclbnd4lem3  13660  faclbnd4  13662  fi1uzind  13860  swrd00  14006  swrd0  14020  cats1un  14083  reuccatpfxs1  14109  cshw0  14156  cshwn  14159  wwlktovfo  14322  shftf  14438  sqrtdiv  14625  leabs  14659  mulcn2  14952  summolem2  15073  fsumrev2  15137  geomulcvg  15232  prodmolem2  15289  zprod  15291  prodsn  15316  prodsnf  15318  fprodle  15350  bpolydiflem  15408  bpoly2  15411  bpoly3  15412  ruclem6  15588  dvdsflip  15667  dvdsfac  15676  gcdcllem1  15846  lcmgcdlem  15948  rpexp1i  16063  hashdvds  16110  hashgcdlem  16123  phisum  16125  iserodd  16170  pcqcl  16191  pcid  16207  ismred  16873  funcpropd  17170  natpropd  17246  lubun  17733  odupos  17745  sgrpidmnd  17916  issubmd  17971  grpinvnzcl  18171  mulgneg  18246  mulgnn0z  18254  symgfixf1  18565  symgsssg  18595  symgfisg  18596  pgpssslw  18739  sylow2alem2  18743  sylow2a  18744  oddvdssubg  18975  gsumzunsnd  19076  gsumunsnfd  19077  gsum2dlem1  19090  gsum2dlem2  19091  gsumcom3  19098  ablfac1eu  19195  pgpfac1lem5  19201  gsumdixp  19362  dvdsrcl2  19403  isdrngd  19527  cnsubrg  20158  psgnodpm  20284  evlslem4  20754  coe1tmmul2  20912  mpomatmul  21058  cpmidpmat  21484  intcld  21651  neiptopnei  21743  ordtrest2lem  21814  lmss  21909  cmpcovf  22002  cncmp  22003  fincmp  22004  cmpsublem  22010  cmpsub  22011  unconn  22040  1stcfb  22056  2ndcsep  22070  refun0  22126  locfincmp  22137  1stckgenlem  22164  ptbasin  22188  ptbasfi  22192  ptunimpt  22206  ptuniconst  22209  dfac14  22229  ptcnp  22233  xkoptsub  22265  xkococnlem  22270  xkoinjcn  22298  qtopcmplem  22318  qtophmeo  22428  fbfinnfr  22452  isufil2  22519  isfcls  22620  xmetrtri  22968  xmetrtri2  22969  blssioo  23406  divcn  23479  bndth  23569  clmvscom  23701  resscdrg  23968  minveclem3  24039  finiunmbl  24154  opnmbllem  24211  ismbf2d  24250  itg2seq  24352  bddiblnc  24451  ellimc2  24486  limcmpt2  24493  limcres  24495  dvlem  24505  dvidlem  24524  dvrec  24564  dveflem  24588  dvlip  24602  coe1mul3  24706  dvtaylp  24971  leibpilem2  25533  leibpi  25534  wilthlem2  25660  basellem3  25674  dchreq  25848  dchrsum  25859  lgsval3  25905  lgsdir2lem4  25918  2sqlem6  26013  rpvmasumlem  26077  dchrisum0fno1  26101  rpvmasum2  26102  pntrsumbnd2  26157  ostthlem1  26217  colmid  26488  lmiisolem  26596  dfcgra2  26630  axcontlem2  26765  axcontlem7  26770  upgrex  26891  umgredg  26937  umgrpredgv  26939  umgredgne  26944  umgredgnlp  26946  usgredgppr  26992  edgssv2  26994  uspgredg2vlem  27019  usgredg2vlem1  27021  upgrres1  27109  nbuhgr2vtx1edgblem  27147  nbusgrf1o0  27165  hashnbusgrnn0  27172  iscplgredg  27213  uhgrvd00  27330  finsumvtxdg2size  27346  wlkepvtx  27456  wlknewwlksn  27679  wwlksnextfun  27690  wwlksnextsurj  27692  elwwlks2ons3im  27746  wwlks2onsym  27750  clwwlkf  27838  fusgreghash2wspv  28126  numclwwlk5lem  28178  grpoidinvlem3  28295  ablo32  28338  ablomuldiv  28341  ablodivdiv  28342  ablodiv32  28344  nvscom  28418  dipassr  28635  htthlem  28706  hsn0elch  29037  shscli  29106  nmopun  29803  branmfn  29894  mdslj1i  30108  mdslj2i  30109  atss  30135  chcv1  30144  dmdbr5ati  30211  snsssng  30289  fnpreimac  30430  fcnvgreu  30432  isoun  30451  fsuppcurry1  30475  fsuppcurry2  30476  fzne1  30525  prodpr  30556  prodtp  30557  pmtrprfv2  30767  isprmidlc  31007  ssmxidllem  31022  ordtrest2NEWlem  31225  esumsplit  31372  esumpad2  31375  esumpcvgval  31397  sigaclcu2  31439  ldgenpisyslem1  31482  volmeas  31550  mbfmco2  31583  omsmeas  31641  oddpwdc  31672  eulerpartlemgvv  31694  ballotlemfc0  31810  ballotlemfcc  31811  prodfzo03  31934  circlemethhgt  31974  bnj521  32067  bnj1109  32118  bnj1294  32149  bnj545  32227  bnj605  32239  bnj594  32244  bnj934  32267  bnj953  32271  bnj1137  32327  bnj1174  32335  bnj1388  32365  subfacp1lem4  32490  erdszelem7  32504  erdszelem8  32505  erdsze2lem2  32511  resconn  32553  cvmsdisj  32577  cvmscld  32580  satf0op  32684  mclsax  32876  climuzcnv  32974  pocnv  33059  trpredmintr  33130  fprlem2  33198  nosupno  33263  cgrid2  33524  btwncom  33535  btwnswapid2  33539  colinearperm1  33583  colinearperm3  33584  colinearperm2  33585  colinearperm4  33586  lineext  33597  colinbtwnle  33639  broutsideof2  33643  outsideofcom  33649  linecom  33671  linerflx2  33672  lineintmo  33678  fwddifn0  33685  hfext  33704  ntruni  33735  clsint2  33737  neibastop1  33767  bj-snsetex  34346  relowlssretop  34728  pibt2  34782  fin2solem  34991  lindsadd  34998  matunitlindflem1  35001  poimirlem4  35009  poimirlem25  35030  poimirlem32  35037  opnmbllem0  35041  mblfinlem3  35044  mbfposadd  35052  itg2addnclem3  35058  ftc1anclem6  35083  ftc1anc  35086  eqfnun  35108  ac6gf  35118  heibor1lem  35195  isdrngo2  35344  unichnidl  35417  isfldidl  35454  cnf1dd  35476  lkrss2N  36413  elpadd0  37053  ltrnu  37365  tendoex  38219  cdlemm10N  38362  dicfnN  38427  dihmeetlem2N  38543  dihlatat  38581  lcfrlem9  38794  uzindd  39212  metakunt12  39310  fsuppind  39393  ismrcd1  39559  isnacs3  39571  pellfundglb  39746  jm2.22  39856  jm2.23  39857  isnumbasgrplem1  39965  hbtlem6  39993  rngunsnply  40037  mnringmulrcld  40860  dvgrat  40940  cvgdvgrat  40941  nznngen  40944  uzmptshftfval  40974  rnmptlb  41809  rnmptbddlem  41810  rnmptbd2lem  41815  iccshift  42085  iooshift  42089  liminflbuz2  42387  xlimbr  42399  itgperiod  42553  fourierdlem42  42721  fourierdlem68  42746  fourierdlem93  42771  elprneb  43551  dfatcolem  43741  ichim  43904  ichnfb  43912  prproropf1olem1  43950  prproropf1olem3  43952  rabsubmgmd  44341  2zlidl  44488  lspsslco  44776
  Copyright terms: Public domain W3C validator