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  147  expi  168  looinv  206  syl6ib  254  syl6ibr  255  syl6bi  256  syl6bir  257  jaoi  857  pm2.37  971  pm2.81  972  oplem1  1057  3jao  1427  impsingle  1635  al2im  1822  exlimdv  1941  19.23v  1950  19.36imvOLD  1954  spimfw  1974  ax13b  2040  nf5-1  2145  hbald  2172  19.8a  2178  spimedv  2195  19.9d  2201  sbequ1  2245  sbft  2266  cbv2w  2337  spimed  2387  cbv2  2402  cbv2h  2405  ax12  2422  axc11n  2425  equvini  2454  sb2  2479  sb4a  2483  mo3  2563  mopick  2626  moexexlem  2627  dvelimdc  2931  necon1ad  2957  necon4bd  2960  rsp2  3134  vtoclgft  3468  mo2icl  3627  2reu1  3809  reuss2  4230  reupick2  4235  elpwunsn  4599  pwpw0  4726  sssn  4739  pwsnOLD  4812  iuneqconst  4915  disjiun  5040  reusv1  5290  reusv3i  5297  ralxfrALT  5308  opth1  5359  copsexgw  5373  copsexg  5374  opelopabt  5413  solin  5493  wefrc  5545  frinxp  5631  ssrelrn  5763  reuop  6156  ordunidif  6261  oneqmini  6264  suctr  6296  ordsssuc2  6301  iotan0  6370  fv3  6735  ndmfv  6747  ssimaex  6796  fvopab3ig  6814  iinpreima  6889  fvcofneq  6912  dff3  6919  dff4  6920  ffnfv  6935  fnsnr  6980  fprb  7009  elunirn  7064  f1mpt  7073  isomin  7146  oprabidw  7244  oprabid  7245  mpoeq123  7283  sorpsscmpl  7522  dfwe2  7559  ssorduni  7563  ssonprc  7571  nlimsucg  7621  ordunisuc2  7623  tfinds  7638  ssnlim  7664  f1oweALT  7745  el2mpocl  7854  f1o2ndf1  7891  frxp  7893  soxp  7896  brtpos  7977  rntpos  7981  dftpos4  7987  onfununi  8078  onnseq  8081  smores2  8091  smo11  8101  tfr3  8135  rdglim2  8168  tz7.48lem  8177  tz7.49  8181  seqomlem2  8187  oawordex  8285  oa00  8287  oaass  8289  om00  8303  odi  8307  omass  8308  oeordi  8315  oelim2  8323  omsmo  8383  eroveu  8494  eceqoveq  8504  map0g  8565  fundmen  8708  sdomdif  8794  onsdominel  8795  nneneq  8829  php3  8832  pssnn  8846  onomeneq  8869  pssnnOLD  8895  f1finf1o  8902  findcard3  8914  unblem1  8923  fiint  8948  ixpfi2  8974  dffi2  9039  elfiun  9046  fisup2g  9084  fiinf2g  9116  wemaplem2  9163  preleqALT  9232  inf3lem2  9244  inf3lem3  9245  inf3lem6  9248  noinfep  9275  dftrpred3g  9339  epfrs  9347  tcmin  9357  r1sdom  9390  tz9.12lem3  9405  rankelb  9440  bndrank  9457  rankunb  9466  rankuni2b  9469  cplem1  9505  karden  9511  carduni  9597  infxpenlem  9627  dfac8alem  9643  alephdom  9695  cardinfima  9711  alephval3  9724  dfac5lem4  9740  dfac5lem5  9741  dfac5  9742  dfac2b  9744  kmlem13  9776  nnadju  9811  ackbij1b  9853  cfub  9863  coflim  9875  cflim2  9877  cfslbn  9881  cfslb2n  9882  cofsmo  9883  cfsmolem  9884  sornom  9891  fincssdom  9937  isf32lem1  9967  isf32lem2  9968  isf32lem9  9975  isf34lem4  9991  isfin1-3  10000  axcc4  10053  domtriomlem  10056  axdc2lem  10062  axdc3lem2  10065  zorn2lem4  10113  zorn2lem6  10115  zornn0g  10119  uniimadom  10158  cardmin  10178  ficard  10179  konigthlem  10182  alephreg  10196  cfpwsdom  10198  axextnd  10205  fpwwe2lem5  10249  fpwwe2lem11  10255  fpwwe2lem12  10256  fpwwe2  10257  canthp1lem2  10267  gchpwdom  10284  winalim2  10310  tskuni  10397  grupr  10411  grur1a  10433  axgroth6  10442  grothomex  10443  eltskm  10457  addclpi  10506  nqereu  10543  ltexnq  10589  nsmallnq  10591  genpn0  10617  genpss  10618  genpnmax  10621  ltaddpr  10648  reclem3pr  10663  reclem4pr  10664  suplem1pr  10666  supsrlem  10725  1re  10833  dedekindle  10996  addid1  11012  negn0  11261  negf1o  11262  negfi  11781  sup2  11788  supadd  11800  supmullem1  11802  supmullem2  11803  zmulcl  12226  zeo  12263  uz11  12463  uzwo  12507  eqreznegel  12530  lbzbi  12532  qextlt  12793  qextle  12794  xrsupsslem  12897  xrinfmsslem  12898  supxrun  12906  supxrpnf  12908  supxrunb1  12909  supxrunb2  12910  fzm1  13192  uzrdgfni  13531  hasheqf1oi  13918  hashreshashfun  14006  leisorel  14026  fundmge2nop0  14058  wrdsymb0  14104  swrdnnn0nd  14221  swrdccatin2d  14309  cshinj  14376  repswcshw  14377  rennim  14802  sqrlem6  14811  caubnd  14922  sqreulem  14923  caucvgrlem  15236  fsumcvg  15276  supcvg  15420  prodeq2ii  15475  fprodcvg  15492  prodmo  15498  dvdslelem  15870  bitsinv1lem  16000  bitsshft  16034  smuval2  16041  smupvallem  16042  gcdcllem1  16058  bezoutlem2  16100  bezoutlem3  16101  algcvga  16136  isprm3  16240  isprm5  16264  oddprmdvds  16456  vdwlem13  16546  vdwnnlem1  16548  vdwnnlem3  16550  ramub1lem1  16579  prmgaplem5  16608  imasaddfnlem  17033  divsfval  17052  catpropd  17212  joindmss  17885  meetdmss  17899  psdmrn  18079  odlem1  18927  gexlem1  18968  cygctb  19277  lmodfopnelem1  19935  islss  19971  lspsneq0  20049  lspsneq  20159  psgnodpmr  20552  obselocv  20690  mvrf1  20950  evlseu  21043  mpfrcl  21045  ppttop  21904  epttop  21906  elcls  21970  restntr  22079  cnprest  22186  regsep  22231  nrmsep3  22252  lmmo  22277  cmpsublem  22296  cmpsub  22297  hauscmplem  22303  txcnpi  22505  txcnp  22517  fbun  22737  fbfinnfr  22738  trfbas2  22740  fgcl  22775  filssufilg  22808  ufinffr  22826  isfcls  22906  fclsrest  22921  flimfnfcls  22925  alexsubALTlem2  22945  alexsubALTlem3  22946  alexsubALTlem4  22947  alexsubALT  22948  cnextcn  22964  imasf1oxms  23387  metequiv2  23408  tngngpim  23557  iccpnfcnv  23841  iccpnfhmeo  23842  iscau2  24174  caun0  24178  minveclem3b  24325  itg1climres  24612  mbfi1fseqlem4  24616  ellimc3  24776  limccnp2  24789  dvlip  24890  itgsubstlem  24945  elply2  25090  coefv0  25142  coemulc  25149  ulmss  25289  sineq0  25413  scvxcvx  25868  sqf11  26021  ppiublem1  26083  fsumvma  26094  2sq2  26314  ostth  26520  mptelee  26986  brbtwn2  26996  colinearalg  27001  axcontlem4  27058  upgrres1  27401  usgr2trlncl  27847  umgrclwwlkge2  28074  upgr4cycl4dv4e  28268  1to3vfriendship  28364  3cyclfrgrrn1  28368  n4cyclfrgr  28374  frgrncvvdeqlem8  28389  frgrwopreg  28406  2clwwlk2clwwlk  28433  numclwwlk2lem1  28459  frgrreg  28477  frgrogt3nreg  28480  nmcvcn  28776  chlimi  29315  ocsh  29364  shsvs  29404  h1datomi  29662  stcl  30297  stge0  30305  stle1  30306  stm1addi  30326  stm1add3i  30328  cvnsym  30371  mdbr2  30377  dmdbr2  30384  mdsl0  30391  mdsl1i  30402  mdsl2i  30403  cvmdi  30405  atexch  30462  atcvat4i  30478  cdj1i  30514  xrge0iifcnv  31597  esumpr2  31747  sigaclci  31812  cntmeas  31906  mbfmcnt  31947  ballotlemfc0  32171  ballotlemfcc  32172  bnj1379  32523  bnj607  32609  bnj908  32624  bnj938  32630  bnj1174  32696  bnj1280  32713  f1resrcmplf1dlem  32771  fnrelpredd  32774  cusgr3cyclex  32811  loop1cycl  32812  acycgrislfgr  32827  pthacycspth  32832  iccllysconn  32925  satffunlem1lem1  33077  satfvel  33087  sate0fv0  33092  funpsstri  33458  fundmpss  33459  dfon2lem3  33480  dfon2lem4  33481  dfon2lem6  33483  dfon2lem9  33486  dfon2  33487  hbimtg  33501  hbaltg  33502  poxp2  33527  poxp3  33533  poseq  33539  sltres  33602  nosepdmlem  33623  nocvxminlem  33709  nocvxmin  33710  dfrdg4  33990  btwntriv2  34051  btwncomim  34052  btwnswapid  34056  btwnexch3  34059  ifscgr  34083  lineunray  34186  hilbert1.2  34194  cldbnd  34252  tailfb  34303  meran3  34339  arg-ax  34342  ontopbas  34354  onsuct0  34367  limsucncmpi  34371  ordcmp  34373  onint1  34375  bj-syl66ib  34472  bj-gl4  34514  bj-alexim  34545  bj-nfimt  34556  bj-ax6e  34586  bj-hbalt  34600  axc11n11r  34602  bj-nnfim  34665  bj-nnfan  34667  bj-nnfor  34669  bj-nnford  34670  bj-nnflemaa  34681  bj-nnflemae  34683  bj-19.21t  34688  bj-19.23t  34689  bj-19.42t  34692  bj-sbft  34694  bj-hbsb3t  34707  bj-cbv2hv  34716  bj-equsal1t  34742  bj-0int  35007  bj-bary1lem1  35216  topdifinffinlem  35255  isbasisrelowllem1  35263  isbasisrelowllem2  35264  iooelexlt  35270  finorwe  35290  finxpreclem1  35297  finxpreclem2  35298  isinf2  35313  fvineqsneu  35319  fvineqsneq  35320  pibt2  35325  wl-spae  35417  wl-19.8eqv  35419  wl-nfeqfb  35432  wl-mo3t  35468  wl-ax11-lem3  35475  fin2so  35501  poimirlem29  35543  poimirlem30  35544  poimirlem31  35545  poimirlem32  35546  ismblfin  35555  indexdom  35629  fzmul  35636  heibor1lem  35704  heibor  35716  exidu1  35751  rngoideu  35798  zerdivemp1x  35842  ispridl2  35933  cnf1dd  35985  cnf2dd  35986  cnfn1dd  35987  cnfn2dd  35988  orcomdd  36062  prtlem14  36625  prter2  36632  aev-o  36682  ax12eq  36692  ax12el  36693  ax12indn  36694  ax12indi  36695  lsatn0  36750  lsatcmp  36754  lsatcv0  36782  lfl1dim  36872  lfl1dim2N  36873  lkrss2N  36920  lub0N  36940  glb0N  36944  glbconxN  37129  hl2at  37156  cvrexchlem  37170  cvratlem  37172  cvrat4  37194  psubspi  37498  pointpsubN  37502  elpaddn0  37551  paddasslem17  37587  ispsubcl2N  37698  ldilval  37864  trlord  38320  diaelrnN  38796  cdlemm10N  38869  cdlemn11pre  38961  dihord2pre  38976  dihglblem2N  39045  dihglblem3N  39046  mapdrvallem2  39396  ioin9i8  39895  sn-dtru  39910  sn-sup2  40147  incssnn0  40236  fphpd  40341  rmxycomplete  40442  dford3lem1  40551  iocinico  40746  ensucne0OLD  40822  al3im  40931  brtrclfv2  41012  frege129d  41048  frege60a  41163  frege60c  41208  frege70  41218  rfovcnvf1od  41289  clsk1indlem3  41330  neik0pk1imk0  41334  gneispace  41421  gneispaceel2  41431  gneispacess2  41433  dvconstbi  41625  axc5c4c711toc7  41695  axc5c4c711to11  41696  pm14.24  41723  sbiota1  41725  bi33imp12  41783  bi123imp0  41789  ee233  41812  vk15.4j  41821  ssralv2  41824  alrim3con13v  41826  tratrb  41829  onfrALTlem3  41837  onfrALTlem2  41839  19.41rg  41843  hbimpg  41847  hbalg  41848  ax6e2ndeq  41852  e2  41924  ee223  41927  sspwtrALT  42115  sspwtrALT2  42116  suctrALT2  42130  trintALT  42174  isosctrlem1ALT  42227  fnchoice  42245  mptfnd  42458  stoweidlem62  43278  2reu8i  44277  2reuimp  44279  ffnafv  44335  lswn0  44569  reupr  44647  reuopreuprim  44651  requad2  44748  bgoldbnnsum3prm  44929  bgoldbtbndlem2  44931  bgoldbtbndlem4  44933  ply1mulgsumlem2  45401  iunord  46053  setrec2fun  46069