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

Step	Hyp	Ref	Expression
1		syl6.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
2		syl6.2	. . 3 ⊢ (𝜒 → 𝜃)
3	2	a1i 11	. 2 ⊢ (𝜓 → (𝜒 → 𝜃))
4	1, 3	sylcom 30	1 ⊢ (𝜑 → (𝜓 → 𝜃))

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  145  expi  165  looinv  203  imbitrdi  251  imbitrrdi  252  biimtrdi  253  biimtrrdi  254  jaoi  857  pm2.37  972  pm2.81  973  oplem1  1056  3jao  1427  impsingle  1628  al2im  1815  exlimdv  1934  19.23v  1943  spimfw  1966  ax13b  2033  nf5-1  2147  hbald  2170  19.8a  2183  spimedv  2199  19.9d  2205  sbequ1  2250  sbft  2271  cbv2w  2336  spimed  2387  cbv2  2402  cbv2h  2405  ax12  2422  axc11n  2425  equvini  2454  sb2  2478  sb4a  2479  mo3  2558  mopick  2619  moexexlem  2620  dvelimdc  2917  necon1ad  2943  necon4bd  2946  rsp2  3247  mo2icl  3671  2reu1  3846  reuss2  4274  reupick2  4279  elpwunsn  4635  pwpw0  4763  sssn  4776  iuneqconst  4951  disjiun  5077  reusv1  5333  reusv3i  5340  ralxfrALT  5351  exneq  5376  opth1  5413  copsexgw  5428  copsexg  5429  opelopabt  5470  solin  5549  wefrc  5608  frinxp  5697  ssrelrn  5832  dmcosseq  5914  dmcosseqOLD  5915  reuop  6236  ordunidif  6352  oneqmini  6355  suctr  6390  ordsssuc2  6395  iotan0  6467  fv3  6835  ndmfv  6849  ssimaex  6902  fvopab3ig  6920  iinpreima  6997  fvcofneq  7021  dff3  7028  dff4  7029  ffnfv  7047  fnsnr  7092  fprb  7123  elunirn  7180  f1mpt  7190  isomin  7266  oprabidw  7372  oprabid  7373  mpoeq123  7413  sorpsscmpl  7662  dfwe2  7702  ssorduni  7707  ssonprc  7715  nlimsucg  7767  ordunisuc2  7769  tfinds  7785  ssnlim  7811  f1oweALT  7899  mptcnfimad  7913  el2mpocl  8011  f1o2ndf1  8047  frxp  8051  soxp  8054  poxp2  8068  poxp3  8075  poseq  8083  brtpos  8160  rntpos  8164  dftpos4  8170  onfununi  8256  onnseq  8259  smores2  8269  smo11  8279  tfr3  8313  rdglim2  8346  tz7.48lem  8355  tz7.49  8359  seqomlem2  8365  oawordex  8467  oa00  8469  oaass  8471  om00  8485  odi  8489  omass  8490  oeordi  8497  oelim2  8505  omsmo  8568  eroveu  8731  eceqoveq  8741  map0g  8803  fundmen  8948  sdomdif  9033  onsdominel  9034  pssnn  9073  nneneq  9110  php3  9113  f1finf1o  9152  findcard3  9162  unblem1  9171  fiint  9206  ixpfi2  9229  dffi2  9302  elfiun  9309  fisup2g  9348  fiinf2g  9381  wemaplem2  9428  elirrv  9478  preleqALT  9502  inf3lem2  9514  inf3lem3  9515  inf3lem6  9518  noinfep  9545  epfrs  9616  tcmin  9626  r1sdom  9659  tz9.12lem3  9674  rankelb  9709  bndrank  9726  rankunb  9735  rankuni2b  9738  cplem1  9774  karden  9780  carduni  9866  infxpenlem  9896  dfac8alem  9912  alephdom  9964  cardinfima  9980  alephval3  9993  dfac5lem4  10009  dfac5lem5  10010  dfac5lem4OLD  10011  dfac5  10012  dfac2b  10014  kmlem13  10046  nnadju  10081  ackbij1b  10121  cfub  10132  coflim  10144  cflim2  10146  cfslbn  10150  cfslb2n  10151  cofsmo  10152  cfsmolem  10153  sornom  10160  fincssdom  10206  isf32lem1  10236  isf32lem2  10237  isf32lem9  10244  isf34lem4  10260  isfin1-3  10269  axcc4  10322  domtriomlem  10325  axdc2lem  10331  axdc3lem2  10334  zorn2lem4  10382  zorn2lem6  10384  zornn0g  10388  uniimadom  10427  cardmin  10447  ficard  10448  konigthlem  10451  alephreg  10465  cfpwsdom  10467  axextnd  10474  fpwwe2lem5  10518  fpwwe2lem11  10524  fpwwe2lem12  10525  fpwwe2  10526  canthp1lem2  10536  gchpwdom  10553  winalim2  10579  tskuni  10666  grupr  10680  grur1a  10702  axgroth6  10711  grothomex  10712  eltskm  10726  addclpi  10775  nqereu  10812  ltexnq  10858  nsmallnq  10860  genpn0  10886  genpss  10887  genpnmax  10890  ltaddpr  10917  reclem3pr  10932  reclem4pr  10933  suplem1pr  10935  supsrlem  10994  1re  11104  dedekindle  11269  addrid  11285  negn0  11538  negf1o  11539  negfi  12063  sup2  12070  supadd  12082  supmullem1  12084  supmullem2  12085  zmulcl  12513  zeo  12551  uz11  12749  uzwo  12801  eqreznegel  12824  lbzbi  12826  qextlt  13094  qextle  13095  xrsupsslem  13198  xrinfmsslem  13199  supxrun  13207  supxrpnf  13209  supxrunb1  13210  supxrunb2  13211  fzm1  13499  uzrdgfni  13857  hasheqf1oi  14250  hashreshashfun  14338  leisorel  14359  fundmge2nop0  14401  wrdsymb0  14448  swrdnnn0nd  14556  swrdccatin2d  14643  cshinj  14710  repswcshw  14711  rennim  15138  01sqrexlem6  15146  caubnd  15258  sqreulem  15259  caucvgrlem  15572  fsumcvg  15611  supcvg  15755  prodeq2ii  15810  fprodcvg  15829  prodmo  15835  dvdslelem  16212  bitsinv1lem  16344  bitsshft  16378  smuval2  16385  smupvallem  16386  gcdcllem1  16402  bezoutlem2  16443  bezoutlem3  16444  algcvga  16482  isprm3  16586  isprm5  16610  oddprmdvds  16807  vdwlem13  16897  vdwnnlem1  16899  vdwnnlem3  16901  ramub1lem1  16930  prmgaplem5  16959  imasaddfnlem  17424  divsfval  17443  catpropd  17607  joindmss  18275  meetdmss  18289  psdmrn  18471  odlem1  19440  gexlem1  19484  cygctb  19797  rngisomring1  20379  lmodfopnelem1  20824  islss  20860  lspsneq0  20938  lspsneq  21052  psgnodpmr  21520  obselocv  21658  mvrf1  21916  evlseu  22011  mpfrcl  22013  ppttop  22915  epttop  22917  elcls  22981  restntr  23090  cnprest  23197  regsep  23242  nrmsep3  23263  lmmo  23288  cmpsublem  23307  cmpsub  23308  hauscmplem  23314  txcnpi  23516  txcnp  23528  fbun  23748  fbfinnfr  23749  trfbas2  23751  fgcl  23786  filssufilg  23819  ufinffr  23837  isfcls  23917  fclsrest  23932  flimfnfcls  23936  alexsubALTlem2  23956  alexsubALTlem3  23957  alexsubALTlem4  23958  alexsubALT  23959  cnextcn  23975  imasf1oxms  24397  metequiv2  24418  tngngpim  24567  iccpnfcnv  24862  iccpnfhmeo  24863  iscau2  25197  caun0  25201  minveclem3b  25348  itg1climres  25635  mbfi1fseqlem4  25639  ellimc3  25800  limccnp2  25813  dvlip  25918  itgsubstlem  25975  elply2  26121  coefv0  26173  coemulc  26180  ulmss  26326  sineq0  26453  scvxcvx  26916  sqf11  27069  ppiublem1  27133  fsumvma  27144  2sq2  27364  ostth  27570  sltres  27594  nosepdmlem  27615  nobdaymin  27709  nocvxminlem  27710  addsprop  27912  mptelee  28866  brbtwn2  28876  colinearalg  28881  axcontlem4  28938  upgrres1  29284  usgr2trlncl  29731  umgrclwwlkge2  29961  upgr4cycl4dv4e  30155  1to3vfriendship  30251  3cyclfrgrrn1  30255  n4cyclfrgr  30261  frgrncvvdeqlem8  30276  frgrwopreg  30293  2clwwlk2clwwlk  30320  numclwwlk2lem1  30346  frgrreg  30364  frgrogt3nreg  30367  nmcvcn  30665  chlimi  31204  ocsh  31253  shsvs  31293  h1datomi  31551  stcl  32186  stge0  32194  stle1  32195  stm1addi  32215  stm1add3i  32217  cvnsym  32260  mdbr2  32266  dmdbr2  32273  mdsl0  32280  mdsl1i  32291  mdsl2i  32292  cvmdi  32294  atexch  32351  atcvat4i  32367  cdj1i  32403  1arithufdlem4  33502  xrge0iifcnv  33936  esumpr2  34070  sigaclci  34135  cntmeas  34229  mbfmcnt  34271  ballotlemfc0  34496  ballotlemfcc  34497  bnj1379  34832  bnj607  34918  bnj908  34933  bnj938  34939  bnj1174  35005  bnj1280  35022  f1resrcmplf1dlem  35088  fnrelpredd  35091  axnulg  35094  tz9.1regs  35102  cusgr3cyclex  35148  loop1cycl  35149  acycgrislfgr  35164  pthacycspth  35169  iccllysconn  35262  satffunlem1lem1  35414  satfvel  35424  sate0fv0  35429  antnestlaw2  35704  funpsstri  35778  fundmpss  35779  dfon2lem3  35798  dfon2lem4  35799  dfon2lem6  35801  dfon2lem9  35804  dfon2  35805  hbimtg  35819  hbaltg  35820  dfrdg4  35964  btwntriv2  36025  btwncomim  36026  btwnswapid  36030  btwnexch3  36033  ifscgr  36057  lineunray  36160  hilbert1.2  36168  cldbnd  36339  tailfb  36390  meran3  36426  arg-ax  36429  ontopbas  36441  onsuct0  36454  limsucncmpi  36458  ordcmp  36460  onint1  36462  weiunpo  36478  bj-syl66ib  36568  bj-gl4  36608  bj-alexim  36640  bj-nfimt  36651  bj-ax6e  36681  bj-hbalt  36694  axc11n11r  36696  bj-nnfim  36759  bj-nnfan  36761  bj-nnfor  36763  bj-nnford  36764  bj-nnflemaa  36775  bj-nnflemae  36777  bj-19.21t  36782  bj-19.23t  36783  bj-19.42t  36786  bj-sbft  36788  bj-hbsb3t  36801  bj-cbv2hv  36810  bj-equsal1t  36835  bj-0int  37114  bj-bary1lem1  37324  topdifinffinlem  37360  isbasisrelowllem1  37368  isbasisrelowllem2  37369  iooelexlt  37375  finorwe  37395  finxpreclem1  37402  finxpreclem2  37403  isinf2  37418  fvineqsneu  37424  fvineqsneq  37425  pibt2  37430  wl-spae  37534  wl-19.8eqv  37536  wl-nfeqfb  37549  wl-mo3t  37589  wl-ax11-lem3  37600  fin2so  37626  poimirlem29  37668  poimirlem30  37669  poimirlem31  37670  poimirlem32  37671  ismblfin  37680  indexdom  37753  fzmul  37760  heibor1lem  37828  heibor  37840  exidu1  37875  rngoideu  37922  zerdivemp1x  37966  ispridl2  38057  cnf1dd  38109  cnf2dd  38110  cnfn1dd  38111  cnfn2dd  38112  orcomdd  38186  disjlem14  38815  disjdmqsss  38819  disjdmqscossss  38820  prtlem14  38892  prter2  38899  aev-o  38949  ax12eq  38959  ax12el  38960  ax12indn  38961  ax12indi  38962  lsatn0  39017  lsatcmp  39021  lsatcv0  39049  lfl1dim  39139  lfl1dim2N  39140  lkrss2N  39187  lub0N  39207  glb0N  39211  glbconxN  39396  hl2at  39423  cvrexchlem  39437  cvratlem  39439  cvrat4  39461  psubspi  39765  pointpsubN  39769  elpaddn0  39818  paddasslem17  39854  ispsubcl2N  39965  ldilval  40131  trlord  40587  diaelrnN  41063  cdlemm10N  41136  cdlemn11pre  41228  dihord2pre  41243  dihglblem2N  41312  dihglblem3N  41313  mapdrvallem2  41663  ioin9i8  42219  sn-sup2  42503  incssnn0  42723  fphpd  42828  rmxycomplete  42929  dford3lem1  43038  iocinico  43224  onsupnmax  43240  cantnfresb  43336  cantnf2  43337  tfsconcatb0  43356  tfsconcat0b  43358  sdomne0  43425  sdomne0d  43426  ensucne0OLD  43542  al3im  43659  brtrclfv2  43739  frege129d  43775  frege60a  43890  frege60c  43935  frege70  43945  rfovcnvf1od  44016  clsk1indlem3  44055  neik0pk1imk0  44059  gneispace  44146  gneispaceel2  44156  gneispacess2  44158  dvconstbi  44346  axc5c4c711toc7  44416  axc5c4c711to11  44417  pm14.24  44444  sbiota1  44446  bi33imp12  44503  bi123imp0  44508  ee233  44531  vk15.4j  44540  ssralv2  44543  alrim3con13v  44545  tratrb  44548  onfrALTlem3  44556  onfrALTlem2  44558  19.41rg  44562  hbimpg  44566  hbalg  44567  ax6e2ndeq  44571  e2  44643  ee223  44646  sspwtrALT  44833  sspwtrALT2  44834  suctrALT2  44848  trintALT  44892  isosctrlem1ALT  44945  relpmin  44964  traxext  44989  modelaxreplem2  44991  ssclaxsep  44994  fnchoice  45045  mptfnd  45258  stoweidlem62  46079  2reu8i  47123  2reuimp  47125  ffnafv  47181  lswn0  47454  reupr  47532  reuopreuprim  47536  requad2  47633  bgoldbnnsum3prm  47814  bgoldbtbndlem2  47816  bgoldbtbndlem4  47818  gricsym  47931  gpgedgvtx1  48072  ply1mulgsumlem2  48398  iunord  49687  setrec2fun  49703