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  141  expi  162  looinv  194  syl6ib  242  syl6ibr  243  syl6bi  244  syl6bir  245  syl6an  666  jaoi  875  pm2.37  984  pm2.81  985  oplem1  1072  3jao  1542  3jaoOLD  1543  al2im  1899  nfimdOLDOLD  1985  exlimdv  2024  19.23v  2034  19.36imv  2036  spimfw  2059  ax13b  2132  nf5-1  2190  hbald  2209  19.9d  2237  19.9dOLDOLD  2238  19.9ht  2322  spimed  2431  cbv2h  2444  axc15  2473  ax12  2474  axc11n  2476  equvini  2506  hbsb2  2520  dfsb2  2534  sbequi  2536  sbft  2540  sbi1  2553  mo3  2677  mopick  2706  moexex  2712  dvelimdc  2977  necon1ad  3002  necon4bd  3005  rsp2  3131  mo2icl  3590  reuss2  4115  reupick2  4121  elpwunsn  4424  pwpw0  4541  sssn  4554  pwsnALT  4630  dfiun2g  4751  disjiun  4839  axsep  4981  reusv1  5073  reusv3i  5080  ralxfrALT  5091  opth1  5140  copsexg  5152  opelopabt  5189  wefrc  5312  frinxp  5393  ssrelrn  5523  idrefOLD  5727  ordunidif  5992  oneqmini  5995  suctr  6027  ordsssuc2  6032  fv3  6429  ndmfv  6441  ssimaex  6487  fvopab3ig  6502  iinpreima  6570  fvcofneq  6592  dff3  6597  dff4  6598  ffnfv  6613  fnsnr  6659  elunirn  6736  f1mpt  6745  isomin  6814  oprabid  6908  mpt2eq123  6947  sorpsscmpl  7181  dfwe2  7214  ssorduni  7218  ssonprc  7225  nlimsucg  7275  ordunisuc2  7277  tfinds  7292  ssnlim  7316  fun11iun  7359  f1oweALT  7385  el2mpt2cl  7487  f1o2ndf1  7522  frxp  7524  soxp  7527  brtpos  7599  rntpos  7603  dftpos4  7609  onfununi  7677  onnseq  7680  smores2  7690  smo11  7700  tfr3  7734  rdglim2  7767  tz7.48lem  7775  tz7.49  7779  seqomlem2  7785  oawordex  7877  oa00  7879  oaass  7881  om00  7895  odi  7899  omass  7900  oeordi  7907  oelim2  7915  omsmo  7974  eroveu  8081  eceqoveq  8091  map0g  8136  fundmen  8269  sdomdif  8350  onsdominel  8351  nneneq  8385  php3  8388  onomeneq  8392  pssnn  8420  f1finf1o  8429  findcard3  8445  unblem1  8454  fiint  8479  ixpfi2  8506  dffi2  8571  elfiun  8578  fisup2g  8616  fiinf2g  8648  wemaplem2  8694  preleqALT  8762  preleqOLD  8764  inf3lem2  8776  inf3lem3  8777  inf3lem6  8780  noinfep  8807  epfrs  8857  tcmin  8867  r1sdom  8887  r1ord3g  8892  r1ord2  8894  tz9.12lem3  8902  rankelb  8937  bndrank  8954  rankunb  8963  rankuni2b  8966  cplem1  9002  karden  9008  carduni  9093  infxpenlem  9122  dfac8alem  9138  alephdom  9190  cardinfima  9206  alephval3  9219  dfac5lem4  9235  dfac5lem5  9236  dfac5  9237  dfac2b  9239  dfac2OLD  9241  kmlem13  9272  ackbij1b  9349  cfub  9359  coflim  9371  cflim2  9373  cfslbn  9377  cfslb2n  9378  cofsmo  9379  cfsmolem  9380  sornom  9387  fincssdom  9433  isf32lem1  9463  isf32lem2  9464  isf32lem9  9471  isf34lem4  9487  isfin1-3  9496  axcc4  9549  domtriomlem  9552  axdc2lem  9558  axdc3lem2  9561  zorn2lem4  9609  zorn2lem6  9611  zornn0g  9615  axdclem2  9630  uniimadom  9654  cardmin  9674  ficard  9675  konigthlem  9678  alephreg  9692  cfpwsdom  9694  axextnd  9701  fpwwe2lem6  9745  fpwwe2lem12  9751  fpwwe2lem13  9752  fpwwe2  9753  canthp1lem2  9763  winalim2  9806  tskuni  9893  grupr  9907  grur1a  9929  axgroth6  9938  grothomex  9939  eltskm  9953  addclpi  10002  nqereu  10039  ltexnq  10085  nsmallnq  10087  genpn0  10113  genpss  10114  genpnmax  10117  ltaddpr  10144  reclem3pr  10159  reclem4pr  10160  suplem1pr  10162  supsrlem  10220  1re  10328  dedekindle  10489  addid1  10504  negn0  10747  negf1o  10748  negfi  11259  fiminre  11260  sup2  11267  supadd  11279  supmullem1  11281  supmullem2  11282  zmulcl  11695  zeo  11732  uz11  11930  uzwo  11973  eqreznegel  11996  lbzbi  11998  qextlt  12255  qextle  12256  xrsupsslem  12358  xrinfmsslem  12359  supxrun  12367  supxrpnf  12369  supxrunb1  12370  supxrunb2  12371  fzm1  12646  uzrdgfni  12984  hasheqf1oi  13363  hashreshashfun  13446  leisorel  13464  fundmge2nop0  13494  wrdsymb0  13553  swrdccatin2d  13727  cshinj  13784  repswcshw  13785  rennim  14205  sqrlem6  14214  caubnd  14324  sqreulem  14325  rlimclim  14503  caucvgrlem  14629  fsumcvg  14669  supcvg  14813  prodeq2ii  14867  fprodcvg  14884  prodmo  14890  dvdslelem  15257  bitsinv1lem  15385  bitsshft  15419  smuval2  15426  smupvallem  15427  gcdcllem1  15443  bezoutlem2  15479  bezoutlem3  15480  algcvga  15514  isprm3  15617  isprm5  15639  oddprmdvds  15827  vdwlem13  15917  vdwnnlem1  15919  vdwnnlem3  15921  ramub1lem1  15950  prmgaplem5  15979  imasaddfnlem  16396  divsfval  16415  catpropd  16576  joindmss  17215  meetdmss  17229  psdmrn  17415  odlem1  18158  gexlem1  18198  cygctb  18497  lmodfopnelem1  19106  islss  19142  lspsneq0  19222  lspsneq  19332  mvrf1  19637  evlseu  19727  mpfrcl  19729  psgnodpmr  20146  obselocv  20286  ppttop  21029  epttop  21031  elcls  21095  restntr  21204  cnprest  21311  regsep  21356  nrmsep3  21377  lmmo  21402  cmpsublem  21420  cmpsub  21421  hauscmplem  21427  txcnpi  21629  txcnp  21641  fbun  21861  fbfinnfr  21862  trfbas2  21864  fgcl  21899  filssufilg  21932  ufinffr  21950  isfcls  22030  fclsrest  22045  flimfnfcls  22049  alexsubALTlem2  22069  alexsubALTlem3  22070  alexsubALTlem4  22071  alexsubALT  22072  cnextcn  22088  imasf1oxms  22511  metequiv2  22532  tngngpim  22680  iccpnfcnv  22960  iccpnfhmeo  22961  iscau2  23292  caun0  23296  minveclem3b  23417  itg1climres  23701  mbfi1fseqlem4  23705  ellimc3  23863  limccnp2  23876  dvlip  23976  itgsubstlem  24031  elply2  24172  coefv0  24224  coemulc  24231  ulmss  24371  sineq0  24494  scvxcvx  24932  sqf11  25085  ppiublem1  25147  fsumvma  25158  ostth  25548  mptelee  25995  brbtwn2  26005  colinearalg  26010  axcontlem4  26067  upgrres1  26427  usgr2trlncl  26890  umgrclwwlkge2  27140  clwlksfclwwlkOLD  27242  clwwlknunOLD  27292  upgr4cycl4dv4e  27364  1to3vfriendship  27462  3cyclfrgrrn1  27466  n4cyclfrgr  27472  frgrncvvdeqlem8  27487  frgrwopreg  27504  2clwwlk2clwwlk  27533  numclwwlk2lem1  27562  numclwwlk2lem1OLD  27569  frgrreg  27588  frgrogt3nreg  27591  nmcvcn  27884  chlimi  28425  ocsh  28476  shsvs  28516  h1datomi  28774  stcl  29409  stge0  29417  stle1  29418  stm1addi  29438  stm1add3i  29440  cvnsym  29483  mdbr2  29489  dmdbr2  29496  mdsl0  29503  mdsl1i  29514  mdsl2i  29515  cvmdi  29517  atexch  29574  atcvat4i  29590  cdj1i  29626  xrge0iifcnv  30310  esumpr2  30460  sigaclci  30526  cntmeas  30620  mbfmcnt  30661  ballotlemfc0  30885  ballotlemfcc  30886  bnj1379  31229  bnj607  31314  bnj908  31329  bnj938  31335  bnj1174  31399  bnj1280  31416  iccllysconn  31560  funpsstri  31990  fundmpss  31991  fprb  31996  dfon2lem3  32015  dfon2lem4  32016  dfon2lem6  32018  dfon2lem9  32021  dfon2  32022  hbimtg  32037  hbaltg  32038  dftrpred3g  32058  poseq  32079  frrlem5b  32111  frrlem5d  32113  sltres  32141  nosepdmlem  32159  nocvxminlem  32219  nocvxmin  32220  dfrdg4  32384  btwntriv2  32445  btwncomim  32446  btwnswapid  32450  btwnexch3  32453  ifscgr  32477  lineunray  32580  hilbert1.2  32588  cldbnd  32647  tailfb  32698  meran3  32734  arg-ax  32737  ontopbas  32749  onsuct0  32762  limsucncmpi  32766  ordcmp  32768  onint1  32770  bj-syl66ib  32861  bj-gl4  32900  bj-alrimhi  32924  bj-alexim  32925  bj-nfimt  32937  bj-ax6e  32973  bj-hbalt  32991  axc11n11r  32993  bj-hbsb3t  33032  bj-spimedv  33039  bj-cbv2hv  33050  bj-sbftv  33081  bj-axsep  33109  bj-equsal1t  33124  bj-mo3OLD  33147  bj-0int  33368  bj-bary1lem1  33480  topdifinffinlem  33513  isbasisrelowllem1  33521  isbasisrelowllem2  33522  iooelexlt  33528  finxpreclem1  33544  finxpreclem2  33545  wl-spae  33624  wl-19.8eqv  33626  wl-nfeqfb  33639  wl-lem-moexsb  33666  wl-mo3t  33674  wl-ax11-lem3  33680  fin2so  33711  poimirlem29  33753  poimirlem30  33754  poimirlem31  33755  poimirlem32  33756  ismblfin  33765  indexdom  33843  fzmul  33850  heibor1lem  33921  heibor  33933  exidu1  33968  rngoideu  34015  zerdivemp1x  34059  ispridl2  34150  orcomdd  34204  cnf1dd  34205  cnfn1dd  34207  cnfn2dd  34208  prtlem14  34655  prter2  34662  aev-o  34712  ax12eq  34722  ax12el  34723  ax12indn  34724  ax12indi  34725  lsatn0  34781  lsatcmp  34785  lsatcv0  34813  lfl1dim  34903  lfl1dim2N  34904  lkrss2N  34951  lub0N  34971  glb0N  34975  glbconxN  35160  hl2at  35187  cvrexchlem  35201  cvratlem  35203  cvrat4  35225  psubspi  35529  pointpsubN  35533  elpaddn0  35582  paddasslem17  35618  ispsubcl2N  35729  ldilval  35895  trlord  36351  diaelrnN  36827  cdlemm10N  36900  cdlemn11pre  36992  dihord2pre  37007  dihglblem2N  37076  dihglblem3N  37077  mapdrvallem2  37427  ioin9i8  37749  incssnn0  37777  fphpd  37883  rmxycomplete  37984  dford3lem1  38095  iocinico  38298  al3im  38439  brtrclfv2  38520  frege129d  38556  frege60a  38673  frege60c  38718  frege70  38728  rfovcnvf1od  38799  clsk1indlem3  38842  neik0pk1imk0  38846  gneispace  38933  gneispaceel2  38943  gneispacess2  38945  dvconstbi  39034  axc5c4c711toc7  39105  axc5c4c711to11  39106  pm14.24  39133  sbiota1  39135  bi33imp12  39195  bi123imp0  39201  ee233  39224  vk15.4j  39233  ssralv2  39236  alrim3con13v  39242  tratrb  39245  onfrALTlem3  39258  onfrALTlem2  39260  19.41rg  39265  hbimpg  39269  hbalg  39270  ax6e2ndeq  39274  e2  39355  ee223  39358  sspwtrALT  39547  sspwtrALT2  39553  suctrALT2  39567  trintALT  39612  isosctrlem1ALT  39665  fnchoice  39683  mptfnd  39936  stoweidlem62  40759  2reu1  41699  ffnafv  41761  lswn0  41956  bgoldbnnsum3prm  42268  bgoldbtbndlem2  42270  bgoldbtbndlem4  42272  ply1mulgsumlem2  42744  iunord  42991  setrec2fun  43008
  Copyright terms: Public domain W3C validator