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  394  syl6an  567  pm2.37  888  pm2.81  895  oplem1  1006  3jao  1386  al2im  1739  nfimdOLDOLD  1821  exlimdv  1858  spimfw  1875  ax13b  1961  nf5-1  2020  hbald  2038  19.9d  2068  19.9ht  2139  spimed  2254  cbv2h  2268  axc15  2302  ax12  2303  axc11n  2306  axc11nOLD  2307  axc11nOLDOLD  2308  axc11nALT  2309  ax12v2OLD  2341  equvini  2345  hbsb2  2358  dfsb2  2372  sbequi  2374  sbft  2378  sbi1  2391  mo3  2506  mopick  2534  moexex  2540  dvelimdc  2782  necon1ad  2807  necon4bd  2810  rsp2  2932  mo2icl  3372  reuss2  3889  reupick2  3895  elpwunsn  4202  pwpw0  4319  sssn  4333  pwsnALT  4404  dfiun2g  4525  disjiun  4613  axsep  4750  reusv1  4836  reusv3i  4845  ralxfrALT  4857  opth1  4914  copsexg  4926  opelopabt  4957  wefrc  5078  frinxp  5155  ssrelrn  5285  issref  5478  ordunidif  5742  oneqmini  5745  suctr  5777  suctrOLD  5778  ordsssuc2  5783  fv3  6173  ndmfv  6185  ssimaex  6230  fvopab3ig  6245  iinpreima  6311  fvcofneq  6333  dff3  6338  dff4  6339  ffnfv  6354  fnsnb  6397  elunirn  6474  f1mpt  6483  isomin  6552  oprabid  6642  mpt2eq123  6679  sorpsscmpl  6913  dfwe2  6943  ssorduni  6947  ssonprc  6954  nlimsucg  7004  ordunisuc2  7006  tfinds  7021  ssnlim  7045  fun11iun  7088  f1oweALT  7112  el2mpt2cl  7211  f1o2ndf1  7245  frxp  7247  soxp  7250  brtpos  7321  rntpos  7325  dftpos4  7331  onfununi  7398  onnseq  7401  smores2  7411  smo11  7421  tfr3  7455  rdglim2  7488  tz7.48lem  7496  tz7.49  7500  seqomlem2  7506  oawordex  7597  oa00  7599  oaass  7601  om00  7615  odi  7619  omass  7620  oeordi  7627  oelim2  7635  omsmo  7694  eroveu  7802  eceqoveq  7813  map0g  7857  fundmen  7990  sdomdif  8068  onsdominel  8069  nneneq  8103  php3  8106  onomeneq  8110  pssnn  8138  f1finf1o  8147  findcard3  8163  unblem1  8172  fiint  8197  ixpfi2  8224  dffi2  8289  elfiun  8296  fisup2g  8334  fiinf2g  8366  wemaplem2  8412  preleq  8474  inf3lem2  8486  inf3lem3  8487  inf3lem6  8490  noinfep  8517  epfrs  8567  tcmin  8577  r1sdom  8597  r1ord3g  8602  r1ord2  8604  tz9.12lem3  8612  rankelb  8647  bndrank  8664  rankunb  8673  rankuni2b  8676  cplem1  8712  karden  8718  carduni  8767  infxpenlem  8796  dfac8alem  8812  alephdom  8864  cardinfima  8880  alephval3  8893  dfac5lem4  8909  dfac5lem5  8910  dfac5  8911  dfac2  8913  kmlem13  8944  ackbij1b  9021  cfub  9031  coflim  9043  cflim2  9045  cfslbn  9049  cfslb2n  9050  cofsmo  9051  cfsmolem  9052  sornom  9059  fincssdom  9105  isf32lem1  9135  isf32lem2  9136  isf32lem9  9143  isf34lem4  9159  isfin1-3  9168  axcc4  9221  domtriomlem  9224  axdc2lem  9230  axdc3lem2  9233  zorn2lem4  9281  zorn2lem6  9283  zornn0g  9287  axdclem2  9302  uniimadom  9326  cardmin  9346  ficard  9347  konigthlem  9350  alephreg  9364  cfpwsdom  9366  axextnd  9373  fpwwe2lem6  9417  fpwwe2lem12  9423  fpwwe2lem13  9424  fpwwe2  9425  canthp1lem2  9435  winalim2  9478  tskuni  9565  grupr  9579  grur1a  9601  axgroth6  9610  grothomex  9611  eltskm  9625  addclpi  9674  nqereu  9711  ltexnq  9757  nsmallnq  9759  genpn0  9785  genpss  9786  genpnmax  9789  ltaddpr  9816  reclem3pr  9831  reclem4pr  9832  suplem1pr  9834  supsrlem  9892  1re  9999  dedekindle  10161  addid1  10176  negn0  10419  negf1o  10420  negfi  10931  fiminre  10932  sup2  10939  supadd  10951  supmullem1  10953  supmullem2  10954  zmulcl  11386  zeo  11423  uz11  11670  uzwo  11711  eqreznegel  11734  lbzbi  11736  qextlt  11993  qextle  11994  xrsupsslem  12096  xrinfmsslem  12097  supxrun  12105  supxrpnf  12107  supxrunb1  12108  supxrunb2  12109  fzm1  12377  uzrdgfni  12713  hasheqf1oi  13096  hasheqf1oiOLD  13097  leisorel  13198  fundmge2nop0  13229  wrdsymb0  13294  swrdccatin2d  13453  cshinj  13510  repswcshw  13511  rennim  13929  sqrlem6  13938  caubnd  14048  sqreulem  14049  rlimclim  14227  caucvgrlem  14353  fsumcvg  14392  supcvg  14532  prodeq2ii  14587  fprodcvg  14604  prodmo  14610  dvdslelem  14974  bitsinv1lem  15106  bitsshft  15140  smuval2  15147  smupvallem  15148  gcdcllem1  15164  bezoutlem2  15200  bezoutlem3  15201  algcvga  15235  isprm3  15339  isprm5  15362  oddprmdvds  15550  vdwlem13  15640  vdwnnlem1  15642  vdwnnlem3  15644  ramub1lem1  15673  prmgaplem5  15702  imasaddfnlem  16128  divsfval  16147  catpropd  16309  joindmss  16947  meetdmss  16961  psdmrn  17147  odlem1  17894  gexlem1  17934  cygctb  18233  lmodfopnelem1  18839  islss  18875  lspsneq0  18952  lspsneq  19062  mvrf1  19365  evlseu  19456  mpfrcl  19458  psgnodpmr  19876  obselocv  20012  ppttop  20751  epttop  20753  elcls  20817  restntr  20926  cnprest  21033  regsep  21078  nrmsep3  21099  lmmo  21124  cmpsublem  21142  cmpsub  21143  hauscmplem  21149  txcnpi  21351  txcnp  21363  fbun  21584  fbfinnfr  21585  trfbas2  21587  fgcl  21622  filssufilg  21655  ufinffr  21673  isfcls  21753  fclsrest  21768  flimfnfcls  21772  alexsubALTlem2  21792  alexsubALTlem3  21793  alexsubALTlem4  21794  alexsubALT  21795  cnextcn  21811  imasf1oxms  22234  metequiv2  22255  tngngpim  22403  iccpnfcnv  22683  iccpnfhmeo  22684  iscau2  23015  caun0  23019  minveclem3b  23139  itg1climres  23421  mbfi1fseqlem4  23425  ellimc3  23583  limccnp2  23596  dvlip  23694  itgsubstlem  23749  elply2  23890  coefv0  23942  coemulc  23949  ulmss  24089  sineq0  24211  scvxcvx  24646  sqf11  24799  ppiublem1  24861  fsumvma  24872  ostth  25262  mptelee  25709  brbtwn2  25719  colinearalg  25724  axcontlem4  25781  upgrres1  26127  usgr2trlncl  26559  umgrclwwlksge2  26812  clwlksfclwwlk  26862  clwwlksnun  26874  upgr4cycl4dv4e  26945  1to3vfriendship  27043  3cyclfrgrrn1  27047  n4cyclfrgr  27053  frgrncvvdeqlemB  27069  frgr2wwlk1  27086  numclwwlkovf2ex  27109  numclwwlk2lem1  27124  frgrreg  27140  frgrogt3nreg  27143  nmcvcn  27438  chlimi  27979  ocsh  28030  shsvs  28070  h1datomi  28328  stcl  28963  stge0  28971  stle1  28972  stm1addi  28992  stm1add3i  28994  cvnsym  29037  mdbr2  29043  dmdbr2  29050  mdsl0  29057  mdsl1i  29068  mdsl2i  29069  cvmdi  29071  atexch  29128  atcvat4i  29144  cdj1i  29180  xrge0iifcnv  29803  esumpr2  29952  sigaclci  30018  cntmeas  30112  mbfmcnt  30153  ballotlemfc0  30377  ballotlemfcc  30378  bnj142OLD  30555  bnj1379  30662  bnj607  30747  bnj908  30762  bnj938  30768  bnj1174  30832  bnj1280  30849  iccllysconn  30993  funpsstri  31420  fundmpss  31421  fprb  31426  dfon2lem3  31444  dfon2lem4  31445  dfon2lem6  31447  dfon2lem9  31450  dfon2  31451  hbimtg  31466  hbaltg  31467  dftrpred3g  31487  poseq  31504  frrlem5b  31539  frrlem5d  31541  sltres  31571  nocvxminlem  31606  nocvxmin  31607  nosepdmlem  31620  dfrdg4  31753  btwntriv2  31814  btwncomim  31815  btwnswapid  31819  btwnexch3  31822  ifscgr  31846  lineunray  31949  hilbert1.2  31957  cldbnd  32016  tailfb  32067  meran3  32107  arg-ax  32110  ontopbas  32122  onsuct0  32135  limsucncmpi  32139  ordcmp  32141  onint1  32143  bj-gl4  32275  bj-alrimhi  32299  bj-alexim  32300  bj-ax6e  32348  bj-hbalt  32366  axc11n11r  32368  bj-hbsb3t  32407  bj-spimedv  32414  bj-cbv2hv  32426  bj-sbftv  32459  bj-axsep  32489  bj-equsal1t  32505  bj-mo3OLD  32530  bj-syl66ib  32531  bj-bary1lem1  32833  topdifinffinlem  32866  isbasisrelowllem1  32874  isbasisrelowllem2  32875  iooelexlt  32881  finxpreclem1  32897  finxpreclem2  32898  wl-spae  32977  wl-19.8eqv  32980  wl-nfeqfb  32994  wl-lem-moexsb  33021  wl-mo3t  33029  wl-ax11-lem3  33035  fin2so  33067  poimirlem29  33109  poimirlem30  33110  poimirlem31  33111  poimirlem32  33112  ismblfin  33121  indexdom  33200  fzmul  33208  heibor1lem  33279  heibor  33291  exidu1  33326  rngoideu  33373  zerdivemp1x  33417  ispridl2  33508  orcomdd  33562  cnf1dd  33563  cnfn1dd  33565  cnfn2dd  33566  prtlem14  33678  prter2  33685  aev-o  33735  ax12eq  33745  ax12el  33746  ax12indn  33747  ax12indi  33748  lsatn0  33805  lsatcmp  33809  lsatcv0  33837  lfl1dim  33927  lfl1dim2N  33928  lkrss2N  33975  lub0N  33995  glb0N  33999  glbconxN  34183  hl2at  34210  cvrexchlem  34224  cvratlem  34226  cvrat4  34248  psubspi  34552  pointpsubN  34556  elpaddn0  34605  paddasslem17  34641  ispsubcl2N  34752  ldilval  34918  trlord  35376  diaelrnN  35853  cdlemm10N  35926  cdlemn11pre  36018  dihord2pre  36033  dihglblem2N  36102  dihglblem3N  36103  mapdrvallem2  36453  incssnn0  36793  fphpd  36899  rmxycomplete  37001  dford3lem1  37112  iocinico  37317  al3im  37458  brtrclfv2  37539  frege129d  37575  frege60a  37693  frege60c  37738  frege70  37748  rfovcnvf1od  37819  clsk1indlem3  37862  neik0pk1imk0  37866  gneispace  37953  gneispaceel2  37963  gneispacess2  37965  dvconstbi  38054  axc5c4c711toc7  38126  axc5c4c711to11  38127  pm14.24  38154  sbiota1  38156  bi33imp12  38217  bi123imp0  38223  ee233  38246  vk15.4j  38255  ssralv2  38258  alrim3con13v  38264  tratrb  38267  onfrALTlem3  38280  onfrALTlem2  38282  19.41rg  38287  hbimpg  38291  hbalg  38292  ax6e2ndeq  38296  e2  38377  ee223  38380  sspwtrALT  38571  sspwtrALT2  38580  suctrALT2  38594  trintALT  38639  isosctrlem1ALT  38692  fnchoice  38710  mptfnd  38961  stoweidlem62  39616  2reu1  40520  ffnafv  40585  lswn0  40708  bgoldbnnsum3prm  41011  bgoldbtbndlem2  41013  bgoldbtbndlem4  41015  ply1mulgsumlem2  41493  iunord  41744  setrec2fun  41762
  Copyright terms: Public domain W3C validator