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

Theorem syl6 35
Description: A syllogism rule of inference. The second premise is used to replace the consequent of the first premise. (Contributed by NM, 5-Jan-1993.) (Proof shortened by Wolf Lammen, 30-Jul-2012.)
Hypotheses
Ref Expression
syl6.1 (𝜑 → (𝜓𝜒))
syl6.2 (𝜒𝜃)
Assertion
Ref Expression
syl6 (𝜑 → (𝜓𝜃))

Proof of Theorem syl6
StepHypRef Expression
1 syl6.1 . 2 (𝜑 → (𝜓𝜒))
2 syl6.2 . . 3 (𝜒𝜃)
32a1i 11 . 2 (𝜓 → (𝜒𝜃))
41, 3sylcom 30 1 (𝜑 → (𝜓𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
This theorem is referenced by:  syl56  36  syl6com  37  a1dd  50  syl6mpi  67  syl6c  70  syl10  79  com34  91  con1d  139  expi  161  looinv  194  syl6ib  241  syl6ibr  242  syl6bi  243  syl6bir  244  jaoi  393  syl6an  567  pm2.37  907  pm2.81  914  oplem1  1027  3jao  1429  al2im  1782  nfimdOLDOLD  1864  exlimdv  1901  19.23v  1911  19.36imv  1913  spimfw  1935  ax13b  2006  nf5-1  2063  hbald  2081  19.9d  2108  19.9ht  2181  spimed  2291  cbv2h  2305  axc15  2339  ax12  2340  axc11n  2342  axc11nOLD  2343  equvini  2374  hbsb2  2387  dfsb2  2401  sbequi  2403  sbft  2407  sbi1  2420  mo3  2536  mopick  2564  moexex  2570  dvelimdc  2815  necon1ad  2840  necon4bd  2843  rsp2  2965  mo2icl  3418  reuss2  3940  reupick2  3946  elpwunsn  4256  pwpw0  4376  sssn  4390  pwsnALT  4461  dfiun2g  4584  disjiun  4672  axsep  4813  reusv1  4896  reusv3i  4905  ralxfrALT  4917  opth1  4973  copsexg  4985  opelopabt  5016  wefrc  5137  frinxp  5218  ssrelrn  5347  issref  5544  ordunidif  5811  oneqmini  5814  suctr  5846  suctrOLD  5847  ordsssuc2  5852  fv3  6244  ndmfv  6256  ssimaex  6302  fvopab3ig  6317  iinpreima  6385  fvcofneq  6407  dff3  6412  dff4  6413  ffnfv  6428  fnsnr  6472  elunirn  6549  f1mpt  6558  isomin  6627  oprabid  6717  mpt2eq123  6756  sorpsscmpl  6990  dfwe2  7023  ssorduni  7027  ssonprc  7034  nlimsucg  7084  ordunisuc2  7086  tfinds  7101  ssnlim  7125  fun11iun  7168  f1oweALT  7194  el2mpt2cl  7296  f1o2ndf1  7330  frxp  7332  soxp  7335  brtpos  7406  rntpos  7410  dftpos4  7416  onfununi  7483  onnseq  7486  smores2  7496  smo11  7506  tfr3  7540  rdglim2  7573  tz7.48lem  7581  tz7.49  7585  seqomlem2  7591  oawordex  7682  oa00  7684  oaass  7686  om00  7700  odi  7704  omass  7705  oeordi  7712  oelim2  7720  omsmo  7779  eroveu  7885  eceqoveq  7895  map0g  7939  fundmen  8071  sdomdif  8149  onsdominel  8150  nneneq  8184  php3  8187  onomeneq  8191  pssnn  8219  f1finf1o  8228  findcard3  8244  unblem1  8253  fiint  8278  ixpfi2  8305  dffi2  8370  elfiun  8377  fisup2g  8415  fiinf2g  8447  wemaplem2  8493  preleq  8552  inf3lem2  8564  inf3lem3  8565  inf3lem6  8568  noinfep  8595  epfrs  8645  tcmin  8655  r1sdom  8675  r1ord3g  8680  r1ord2  8682  tz9.12lem3  8690  rankelb  8725  bndrank  8742  rankunb  8751  rankuni2b  8754  cplem1  8790  karden  8796  carduni  8845  infxpenlem  8874  dfac8alem  8890  alephdom  8942  cardinfima  8958  alephval3  8971  dfac5lem4  8987  dfac5lem5  8988  dfac5  8989  dfac2  8991  kmlem13  9022  ackbij1b  9099  cfub  9109  coflim  9121  cflim2  9123  cfslbn  9127  cfslb2n  9128  cofsmo  9129  cfsmolem  9130  sornom  9137  fincssdom  9183  isf32lem1  9213  isf32lem2  9214  isf32lem9  9221  isf34lem4  9237  isfin1-3  9246  axcc4  9299  domtriomlem  9302  axdc2lem  9308  axdc3lem2  9311  zorn2lem4  9359  zorn2lem6  9361  zornn0g  9365  axdclem2  9380  uniimadom  9404  cardmin  9424  ficard  9425  konigthlem  9428  alephreg  9442  cfpwsdom  9444  axextnd  9451  fpwwe2lem6  9495  fpwwe2lem12  9501  fpwwe2lem13  9502  fpwwe2  9503  canthp1lem2  9513  winalim2  9556  tskuni  9643  grupr  9657  grur1a  9679  axgroth6  9688  grothomex  9689  eltskm  9703  addclpi  9752  nqereu  9789  ltexnq  9835  nsmallnq  9837  genpn0  9863  genpss  9864  genpnmax  9867  ltaddpr  9894  reclem3pr  9909  reclem4pr  9910  suplem1pr  9912  supsrlem  9970  1re  10077  dedekindle  10239  addid1  10254  negn0  10497  negf1o  10498  negfi  11009  fiminre  11010  sup2  11017  supadd  11029  supmullem1  11031  supmullem2  11032  zmulcl  11464  zeo  11501  uz11  11748  uzwo  11789  eqreznegel  11812  lbzbi  11814  qextlt  12072  qextle  12073  xrsupsslem  12175  xrinfmsslem  12176  supxrun  12184  supxrpnf  12186  supxrunb1  12187  supxrunb2  12188  fzm1  12458  uzrdgfni  12797  hasheqf1oi  13180  hashreshashfun  13264  leisorel  13282  fundmge2nop0  13312  wrdsymb0  13371  swrdccatin2d  13546  cshinj  13603  repswcshw  13604  rennim  14023  sqrlem6  14032  caubnd  14142  sqreulem  14143  rlimclim  14321  caucvgrlem  14447  fsumcvg  14487  supcvg  14632  prodeq2ii  14687  fprodcvg  14704  prodmo  14710  dvdslelem  15078  bitsinv1lem  15210  bitsshft  15244  smuval2  15251  smupvallem  15252  gcdcllem1  15268  bezoutlem2  15304  bezoutlem3  15305  algcvga  15339  isprm3  15443  isprm5  15466  oddprmdvds  15654  vdwlem13  15744  vdwnnlem1  15746  vdwnnlem3  15748  ramub1lem1  15777  prmgaplem5  15806  imasaddfnlem  16235  divsfval  16254  catpropd  16416  joindmss  17054  meetdmss  17068  psdmrn  17254  odlem1  18000  gexlem1  18040  cygctb  18339  lmodfopnelem1  18947  islss  18983  lspsneq0  19060  lspsneq  19170  mvrf1  19473  evlseu  19564  mpfrcl  19566  psgnodpmr  19984  obselocv  20120  ppttop  20859  epttop  20861  elcls  20925  restntr  21034  cnprest  21141  regsep  21186  nrmsep3  21207  lmmo  21232  cmpsublem  21250  cmpsub  21251  hauscmplem  21257  txcnpi  21459  txcnp  21471  fbun  21691  fbfinnfr  21692  trfbas2  21694  fgcl  21729  filssufilg  21762  ufinffr  21780  isfcls  21860  fclsrest  21875  flimfnfcls  21879  alexsubALTlem2  21899  alexsubALTlem3  21900  alexsubALTlem4  21901  alexsubALT  21902  cnextcn  21918  imasf1oxms  22341  metequiv2  22362  tngngpim  22510  iccpnfcnv  22790  iccpnfhmeo  22791  iscau2  23121  caun0  23125  minveclem3b  23245  itg1climres  23526  mbfi1fseqlem4  23530  ellimc3  23688  limccnp2  23701  dvlip  23801  itgsubstlem  23856  elply2  23997  coefv0  24049  coemulc  24056  ulmss  24196  sineq0  24318  scvxcvx  24757  sqf11  24910  ppiublem1  24972  fsumvma  24983  ostth  25373  mptelee  25820  brbtwn2  25830  colinearalg  25835  axcontlem4  25892  upgrres1  26250  usgr2trlncl  26712  umgrclwwlkge2  26957  clwlksfclwwlk  27049  clwwlknunOLD  27091  upgr4cycl4dv4e  27163  1to3vfriendship  27261  3cyclfrgrrn1  27265  n4cyclfrgr  27271  frgrncvvdeqlem8  27286  frgrwopreg  27303  2clwwlk2clwwlk  27338  numclwwlk2lem1  27356  numclwwlk2lem1OLD  27363  frgrreg  27381  frgrogt3nreg  27384  nmcvcn  27678  chlimi  28219  ocsh  28270  shsvs  28310  h1datomi  28568  stcl  29203  stge0  29211  stle1  29212  stm1addi  29232  stm1add3i  29234  cvnsym  29277  mdbr2  29283  dmdbr2  29290  mdsl0  29297  mdsl1i  29308  mdsl2i  29309  cvmdi  29311  atexch  29368  atcvat4i  29384  cdj1i  29420  xrge0iifcnv  30107  esumpr2  30257  sigaclci  30323  cntmeas  30417  mbfmcnt  30458  ballotlemfc0  30682  ballotlemfcc  30683  bnj1379  31027  bnj607  31112  bnj908  31127  bnj938  31133  bnj1174  31197  bnj1280  31214  iccllysconn  31358  funpsstri  31789  fundmpss  31790  fprb  31795  dfon2lem3  31814  dfon2lem4  31815  dfon2lem6  31817  dfon2lem9  31820  dfon2  31821  hbimtg  31836  hbaltg  31837  dftrpred3g  31857  poseq  31878  frrlem5b  31910  frrlem5d  31912  sltres  31940  nosepdmlem  31958  nocvxminlem  32018  nocvxmin  32019  dfrdg4  32183  btwntriv2  32244  btwncomim  32245  btwnswapid  32249  btwnexch3  32252  ifscgr  32276  lineunray  32379  hilbert1.2  32387  cldbnd  32446  tailfb  32497  meran3  32537  arg-ax  32540  ontopbas  32552  onsuct0  32565  limsucncmpi  32569  ordcmp  32571  onint1  32573  bj-gl4  32705  bj-alrimhi  32729  bj-alexim  32730  bj-ax6e  32778  bj-hbalt  32796  axc11n11r  32798  bj-hbsb3t  32837  bj-spimedv  32844  bj-cbv2hv  32856  bj-sbftv  32888  bj-axsep  32918  bj-equsal1t  32934  bj-mo3OLD  32957  bj-syl66ib  32958  bj-0int  33180  bj-bary1lem1  33291  topdifinffinlem  33325  isbasisrelowllem1  33333  isbasisrelowllem2  33334  iooelexlt  33340  finxpreclem1  33356  finxpreclem2  33357  wl-spae  33436  wl-19.8eqv  33439  wl-nfeqfb  33453  wl-lem-moexsb  33480  wl-mo3t  33488  wl-ax11-lem3  33494  fin2so  33526  poimirlem29  33568  poimirlem30  33569  poimirlem31  33570  poimirlem32  33571  ismblfin  33580  indexdom  33659  fzmul  33667  heibor1lem  33738  heibor  33750  exidu1  33785  rngoideu  33832  zerdivemp1x  33876  ispridl2  33967  orcomdd  34021  cnf1dd  34022  cnfn1dd  34024  cnfn2dd  34025  prtlem14  34478  prter2  34485  aev-o  34535  ax12eq  34545  ax12el  34546  ax12indn  34547  ax12indi  34548  lsatn0  34604  lsatcmp  34608  lsatcv0  34636  lfl1dim  34726  lfl1dim2N  34727  lkrss2N  34774  lub0N  34794  glb0N  34798  glbconxN  34982  hl2at  35009  cvrexchlem  35023  cvratlem  35025  cvrat4  35047  psubspi  35351  pointpsubN  35355  elpaddn0  35404  paddasslem17  35440  ispsubcl2N  35551  ldilval  35717  trlord  36174  diaelrnN  36651  cdlemm10N  36724  cdlemn11pre  36816  dihord2pre  36831  dihglblem2N  36900  dihglblem3N  36901  mapdrvallem2  37251  incssnn0  37591  fphpd  37697  rmxycomplete  37799  dford3lem1  37910  iocinico  38114  al3im  38255  brtrclfv2  38336  frege129d  38372  frege60a  38489  frege60c  38534  frege70  38544  rfovcnvf1od  38615  clsk1indlem3  38658  neik0pk1imk0  38662  gneispace  38749  gneispaceel2  38759  gneispacess2  38761  dvconstbi  38850  axc5c4c711toc7  38922  axc5c4c711to11  38923  pm14.24  38950  sbiota1  38952  bi33imp12  39013  bi123imp0  39019  ee233  39042  vk15.4j  39051  ssralv2  39054  alrim3con13v  39060  tratrb  39063  onfrALTlem3  39076  onfrALTlem2  39078  19.41rg  39083  hbimpg  39087  hbalg  39088  ax6e2ndeq  39092  e2  39173  ee223  39176  sspwtrALT  39366  sspwtrALT2  39372  suctrALT2  39386  trintALT  39431  isosctrlem1ALT  39484  fnchoice  39502  mptfnd  39765  stoweidlem62  40597  2reu1  41507  ffnafv  41572  lswn0  41705  bgoldbnnsum3prm  42017  bgoldbtbndlem2  42019  bgoldbtbndlem4  42021  ply1mulgsumlem2  42500  iunord  42747  setrec2fun  42764
  Copyright terms: Public domain W3C validator