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  569  pm2.37  925  pm2.81  932  oplem1  1045  3jao  1537  3jaoOLD  1538  al2im  1891  nfimdOLDOLD  1973  exlimdv  2010  19.23v  2020  19.36imv  2022  spimfw  2044  ax13b  2115  nf5-1  2172  hbald  2190  19.9d  2217  19.9ht  2290  spimed  2400  cbv2h  2414  axc15  2448  ax12  2449  axc11n  2451  axc11nOLD  2452  equvini  2483  hbsb2  2496  dfsb2  2510  sbequi  2512  sbft  2516  sbi1  2529  mo3  2645  mopick  2673  moexex  2679  dvelimdc  2924  necon1ad  2949  necon4bd  2952  rsp2  3074  mo2icl  3526  reuss2  4050  reupick2  4056  elpwunsn  4368  pwpw0  4489  sssn  4503  pwsnALT  4581  dfiun2g  4704  disjiun  4792  axsep  4932  reusv1  5015  reusv3i  5024  ralxfrALT  5036  opth1  5092  copsexg  5104  opelopabt  5137  wefrc  5260  frinxp  5341  ssrelrn  5470  issref  5667  ordunidif  5934  oneqmini  5937  suctr  5969  suctrOLD  5970  ordsssuc2  5975  fv3  6367  ndmfv  6379  ssimaex  6425  fvopab3ig  6440  iinpreima  6508  fvcofneq  6530  dff3  6535  dff4  6536  ffnfv  6551  fnsnr  6595  elunirn  6672  f1mpt  6681  isomin  6750  oprabid  6840  mpt2eq123  6879  sorpsscmpl  7113  dfwe2  7146  ssorduni  7150  ssonprc  7157  nlimsucg  7207  ordunisuc2  7209  tfinds  7224  ssnlim  7248  fun11iun  7291  f1oweALT  7317  el2mpt2cl  7419  f1o2ndf1  7453  frxp  7455  soxp  7458  brtpos  7530  rntpos  7534  dftpos4  7540  onfununi  7607  onnseq  7610  smores2  7620  smo11  7630  tfr3  7664  rdglim2  7697  tz7.48lem  7705  tz7.49  7709  seqomlem2  7715  oawordex  7806  oa00  7808  oaass  7810  om00  7824  odi  7828  omass  7829  oeordi  7836  oelim2  7844  omsmo  7903  eroveu  8009  eceqoveq  8019  map0g  8063  fundmen  8195  sdomdif  8273  onsdominel  8274  nneneq  8308  php3  8311  onomeneq  8315  pssnn  8343  f1finf1o  8352  findcard3  8368  unblem1  8377  fiint  8402  ixpfi2  8429  dffi2  8494  elfiun  8501  fisup2g  8539  fiinf2g  8571  wemaplem2  8617  preleqALT  8685  preleqOLD  8687  inf3lem2  8699  inf3lem3  8700  inf3lem6  8703  noinfep  8730  epfrs  8780  tcmin  8790  r1sdom  8810  r1ord3g  8815  r1ord2  8817  tz9.12lem3  8825  rankelb  8860  bndrank  8877  rankunb  8886  rankuni2b  8889  cplem1  8925  karden  8931  carduni  8997  infxpenlem  9026  dfac8alem  9042  alephdom  9094  cardinfima  9110  alephval3  9123  dfac5lem4  9139  dfac5lem5  9140  dfac5  9141  dfac2b  9143  dfac2OLD  9145  kmlem13  9176  ackbij1b  9253  cfub  9263  coflim  9275  cflim2  9277  cfslbn  9281  cfslb2n  9282  cofsmo  9283  cfsmolem  9284  sornom  9291  fincssdom  9337  isf32lem1  9367  isf32lem2  9368  isf32lem9  9375  isf34lem4  9391  isfin1-3  9400  axcc4  9453  domtriomlem  9456  axdc2lem  9462  axdc3lem2  9465  zorn2lem4  9513  zorn2lem6  9515  zornn0g  9519  axdclem2  9534  uniimadom  9558  cardmin  9578  ficard  9579  konigthlem  9582  alephreg  9596  cfpwsdom  9598  axextnd  9605  fpwwe2lem6  9649  fpwwe2lem12  9655  fpwwe2lem13  9656  fpwwe2  9657  canthp1lem2  9667  winalim2  9710  tskuni  9797  grupr  9811  grur1a  9833  axgroth6  9842  grothomex  9843  eltskm  9857  addclpi  9906  nqereu  9943  ltexnq  9989  nsmallnq  9991  genpn0  10017  genpss  10018  genpnmax  10021  ltaddpr  10048  reclem3pr  10063  reclem4pr  10064  suplem1pr  10066  supsrlem  10124  1re  10231  dedekindle  10393  addid1  10408  negn0  10651  negf1o  10652  negfi  11163  fiminre  11164  sup2  11171  supadd  11183  supmullem1  11185  supmullem2  11186  zmulcl  11618  zeo  11655  uz11  11902  uzwo  11944  eqreznegel  11967  lbzbi  11969  qextlt  12227  qextle  12228  xrsupsslem  12330  xrinfmsslem  12331  supxrun  12339  supxrpnf  12341  supxrunb1  12342  supxrunb2  12343  fzm1  12613  uzrdgfni  12951  hasheqf1oi  13334  hashreshashfun  13418  leisorel  13436  fundmge2nop0  13466  wrdsymb0  13525  swrdccatin2d  13700  cshinj  13757  repswcshw  13758  rennim  14178  sqrlem6  14187  caubnd  14297  sqreulem  14298  rlimclim  14476  caucvgrlem  14602  fsumcvg  14642  supcvg  14787  prodeq2ii  14842  fprodcvg  14859  prodmo  14865  dvdslelem  15233  bitsinv1lem  15365  bitsshft  15399  smuval2  15406  smupvallem  15407  gcdcllem1  15423  bezoutlem2  15459  bezoutlem3  15460  algcvga  15494  isprm3  15598  isprm5  15621  oddprmdvds  15809  vdwlem13  15899  vdwnnlem1  15901  vdwnnlem3  15903  ramub1lem1  15932  prmgaplem5  15961  imasaddfnlem  16390  divsfval  16409  catpropd  16570  joindmss  17208  meetdmss  17222  psdmrn  17408  odlem1  18154  gexlem1  18194  cygctb  18493  lmodfopnelem1  19101  islss  19137  lspsneq0  19214  lspsneq  19324  mvrf1  19627  evlseu  19718  mpfrcl  19720  psgnodpmr  20138  obselocv  20274  ppttop  21013  epttop  21015  elcls  21079  restntr  21188  cnprest  21295  regsep  21340  nrmsep3  21361  lmmo  21386  cmpsublem  21404  cmpsub  21405  hauscmplem  21411  txcnpi  21613  txcnp  21625  fbun  21845  fbfinnfr  21846  trfbas2  21848  fgcl  21883  filssufilg  21916  ufinffr  21934  isfcls  22014  fclsrest  22029  flimfnfcls  22033  alexsubALTlem2  22053  alexsubALTlem3  22054  alexsubALTlem4  22055  alexsubALT  22056  cnextcn  22072  imasf1oxms  22495  metequiv2  22516  tngngpim  22664  iccpnfcnv  22944  iccpnfhmeo  22945  iscau2  23275  caun0  23279  minveclem3b  23399  itg1climres  23680  mbfi1fseqlem4  23684  ellimc3  23842  limccnp2  23855  dvlip  23955  itgsubstlem  24010  elply2  24151  coefv0  24203  coemulc  24210  ulmss  24350  sineq0  24472  scvxcvx  24911  sqf11  25064  ppiublem1  25126  fsumvma  25137  ostth  25527  mptelee  25974  brbtwn2  25984  colinearalg  25989  axcontlem4  26046  upgrres1  26404  usgr2trlncl  26866  umgrclwwlkge2  27114  clwlksfclwwlkOLD  27216  clwwlknunOLD  27265  upgr4cycl4dv4e  27337  1to3vfriendship  27435  3cyclfrgrrn1  27439  n4cyclfrgr  27445  frgrncvvdeqlem8  27460  frgrwopreg  27477  2clwwlk2clwwlk  27507  numclwwlk2lem1  27537  numclwwlk2lem1OLD  27544  frgrreg  27562  frgrogt3nreg  27565  nmcvcn  27859  chlimi  28400  ocsh  28451  shsvs  28491  h1datomi  28749  stcl  29384  stge0  29392  stle1  29393  stm1addi  29413  stm1add3i  29415  cvnsym  29458  mdbr2  29464  dmdbr2  29471  mdsl0  29478  mdsl1i  29489  mdsl2i  29490  cvmdi  29492  atexch  29549  atcvat4i  29565  cdj1i  29601  xrge0iifcnv  30288  esumpr2  30438  sigaclci  30504  cntmeas  30598  mbfmcnt  30639  ballotlemfc0  30863  ballotlemfcc  30864  bnj1379  31208  bnj607  31293  bnj908  31308  bnj938  31314  bnj1174  31378  bnj1280  31395  iccllysconn  31539  funpsstri  31970  fundmpss  31971  fprb  31976  dfon2lem3  31995  dfon2lem4  31996  dfon2lem6  31998  dfon2lem9  32001  dfon2  32002  hbimtg  32017  hbaltg  32018  dftrpred3g  32038  poseq  32059  frrlem5b  32091  frrlem5d  32093  sltres  32121  nosepdmlem  32139  nocvxminlem  32199  nocvxmin  32200  dfrdg4  32364  btwntriv2  32425  btwncomim  32426  btwnswapid  32430  btwnexch3  32433  ifscgr  32457  lineunray  32560  hilbert1.2  32568  cldbnd  32627  tailfb  32678  meran3  32718  arg-ax  32721  ontopbas  32733  onsuct0  32746  limsucncmpi  32750  ordcmp  32752  onint1  32754  bj-gl4  32886  bj-alrimhi  32910  bj-alexim  32911  bj-ax6e  32959  bj-hbalt  32977  axc11n11r  32979  bj-hbsb3t  33018  bj-spimedv  33025  bj-cbv2hv  33037  bj-sbftv  33069  bj-axsep  33099  bj-equsal1t  33115  bj-mo3OLD  33138  bj-syl66ib  33139  bj-0int  33361  bj-bary1lem1  33472  topdifinffinlem  33506  isbasisrelowllem1  33514  isbasisrelowllem2  33515  iooelexlt  33521  finxpreclem1  33537  finxpreclem2  33538  wl-spae  33619  wl-19.8eqv  33622  wl-nfeqfb  33636  wl-lem-moexsb  33663  wl-mo3t  33671  wl-ax11-lem3  33677  fin2so  33709  poimirlem29  33751  poimirlem30  33752  poimirlem31  33753  poimirlem32  33754  ismblfin  33763  indexdom  33842  fzmul  33850  heibor1lem  33921  heibor  33933  exidu1  33968  rngoideu  34015  zerdivemp1x  34059  ispridl2  34150  orcomdd  34204  cnf1dd  34205  cnfn1dd  34207  cnfn2dd  34208  prtlem14  34663  prter2  34670  aev-o  34720  ax12eq  34730  ax12el  34731  ax12indn  34732  ax12indi  34733  lsatn0  34789  lsatcmp  34793  lsatcv0  34821  lfl1dim  34911  lfl1dim2N  34912  lkrss2N  34959  lub0N  34979  glb0N  34983  glbconxN  35167  hl2at  35194  cvrexchlem  35208  cvratlem  35210  cvrat4  35232  psubspi  35536  pointpsubN  35540  elpaddn0  35589  paddasslem17  35625  ispsubcl2N  35736  ldilval  35902  trlord  36359  diaelrnN  36836  cdlemm10N  36909  cdlemn11pre  37001  dihord2pre  37016  dihglblem2N  37085  dihglblem3N  37086  mapdrvallem2  37436  incssnn0  37776  fphpd  37882  rmxycomplete  37984  dford3lem1  38095  iocinico  38299  al3im  38440  brtrclfv2  38521  frege129d  38557  frege60a  38674  frege60c  38719  frege70  38729  rfovcnvf1od  38800  clsk1indlem3  38843  neik0pk1imk0  38847  gneispace  38934  gneispaceel2  38944  gneispacess2  38946  dvconstbi  39035  axc5c4c711toc7  39107  axc5c4c711to11  39108  pm14.24  39135  sbiota1  39137  bi33imp12  39198  bi123imp0  39204  ee233  39227  vk15.4j  39236  ssralv2  39239  alrim3con13v  39245  tratrb  39248  onfrALTlem3  39261  onfrALTlem2  39263  19.41rg  39268  hbimpg  39272  hbalg  39273  ax6e2ndeq  39277  e2  39358  ee223  39361  sspwtrALT  39551  sspwtrALT2  39557  suctrALT2  39571  trintALT  39616  isosctrlem1ALT  39669  fnchoice  39687  mptfnd  39950  stoweidlem62  40782  2reu1  41692  ffnafv  41757  lswn0  41890  bgoldbnnsum3prm  42202  bgoldbtbndlem2  42204  bgoldbtbndlem4  42206  ply1mulgsumlem2  42685  iunord  42932  setrec2fun  42949
  Copyright terms: Public domain W3C validator