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  1627  al2im  1814  exlimdv  1933  19.23v  1942  spimfw  1965  ax13b  2032  nf5-1  2146  hbald  2169  19.8a  2182  spimedv  2198  19.9d  2204  sbequ1  2249  sbft  2270  cbv2w  2335  spimed  2386  cbv2  2401  cbv2h  2404  ax12  2421  axc11n  2424  equvini  2453  sb2  2477  sb4a  2478  mo3  2557  mopick  2618  moexexlem  2619  dvelimdc  2916  necon1ad  2942  necon4bd  2945  rsp2  3246  mo2icl  3676  2reu1  3851  reuss2  4279  reupick2  4284  elpwunsn  4638  pwpw0  4767  sssn  4780  iuneqconst  4956  disjiun  5083  reusv1  5339  reusv3i  5346  ralxfrALT  5357  exneq  5382  opth1  5422  copsexgw  5437  copsexg  5438  opelopabt  5479  solin  5558  wefrc  5617  frinxp  5706  ssrelrn  5841  dmcosseq  5923  dmcosseqOLD  5924  reuop  6245  ordunidif  6361  oneqmini  6364  suctr  6399  ordsssuc2  6404  iotan0  6476  fv3  6844  ndmfv  6859  ssimaex  6912  fvopab3ig  6930  iinpreima  7007  fvcofneq  7031  dff3  7038  dff4  7039  ffnfv  7057  fnsnr  7103  fprb  7134  elunirn  7191  f1mpt  7202  isomin  7278  oprabidw  7384  oprabid  7385  mpoeq123  7425  sorpsscmpl  7674  dfwe2  7714  ssorduni  7719  ssonprc  7727  nlimsucg  7782  ordunisuc2  7784  tfinds  7800  ssnlim  7826  f1oweALT  7914  mptcnfimad  7928  el2mpocl  8026  f1o2ndf1  8062  frxp  8066  soxp  8069  poxp2  8083  poxp3  8090  poseq  8098  brtpos  8175  rntpos  8179  dftpos4  8185  onfununi  8271  onnseq  8274  smores2  8284  smo11  8294  tfr3  8328  rdglim2  8361  tz7.48lem  8370  tz7.49  8374  seqomlem2  8380  oawordex  8482  oa00  8484  oaass  8486  om00  8500  odi  8504  omass  8505  oeordi  8512  oelim2  8520  omsmo  8583  eroveu  8746  eceqoveq  8756  map0g  8818  fundmen  8963  sdomdif  9049  onsdominel  9050  pssnn  9092  nneneq  9130  php3  9133  f1finf1o  9174  f1finf1oOLD  9175  findcard3  9187  findcard3OLD  9188  unblem1  9197  fiint  9235  fiintOLD  9236  ixpfi2  9259  dffi2  9332  elfiun  9339  fisup2g  9378  fiinf2g  9411  wemaplem2  9458  elirrv  9508  preleqALT  9532  inf3lem2  9544  inf3lem3  9545  inf3lem6  9548  noinfep  9575  epfrs  9646  tcmin  9656  r1sdom  9689  tz9.12lem3  9704  rankelb  9739  bndrank  9756  rankunb  9765  rankuni2b  9768  cplem1  9804  karden  9810  carduni  9896  infxpenlem  9926  dfac8alem  9942  alephdom  9994  cardinfima  10010  alephval3  10023  dfac5lem4  10039  dfac5lem5  10040  dfac5lem4OLD  10041  dfac5  10042  dfac2b  10044  kmlem13  10076  nnadju  10111  ackbij1b  10151  cfub  10162  coflim  10174  cflim2  10176  cfslbn  10180  cfslb2n  10181  cofsmo  10182  cfsmolem  10183  sornom  10190  fincssdom  10236  isf32lem1  10266  isf32lem2  10267  isf32lem9  10274  isf34lem4  10290  isfin1-3  10299  axcc4  10352  domtriomlem  10355  axdc2lem  10361  axdc3lem2  10364  zorn2lem4  10412  zorn2lem6  10414  zornn0g  10418  uniimadom  10457  cardmin  10477  ficard  10478  konigthlem  10481  alephreg  10495  cfpwsdom  10497  axextnd  10504  fpwwe2lem5  10548  fpwwe2lem11  10554  fpwwe2lem12  10555  fpwwe2  10556  canthp1lem2  10566  gchpwdom  10583  winalim2  10609  tskuni  10696  grupr  10710  grur1a  10732  axgroth6  10741  grothomex  10742  eltskm  10756  addclpi  10805  nqereu  10842  ltexnq  10888  nsmallnq  10890  genpn0  10916  genpss  10917  genpnmax  10920  ltaddpr  10947  reclem3pr  10962  reclem4pr  10963  suplem1pr  10965  supsrlem  11024  1re  11134  dedekindle  11298  addrid  11314  negn0  11567  negf1o  11568  negfi  12092  sup2  12099  supadd  12111  supmullem1  12113  supmullem2  12114  zmulcl  12542  zeo  12580  uz11  12778  uzwo  12830  eqreznegel  12853  lbzbi  12855  qextlt  13123  qextle  13124  xrsupsslem  13227  xrinfmsslem  13228  supxrun  13236  supxrpnf  13238  supxrunb1  13239  supxrunb2  13240  fzm1  13528  uzrdgfni  13883  hasheqf1oi  14276  hashreshashfun  14364  leisorel  14385  fundmge2nop0  14427  wrdsymb0  14474  swrdnnn0nd  14581  swrdccatin2d  14668  cshinj  14735  repswcshw  14736  rennim  15164  01sqrexlem6  15172  caubnd  15284  sqreulem  15285  caucvgrlem  15598  fsumcvg  15637  supcvg  15781  prodeq2ii  15836  fprodcvg  15855  prodmo  15861  dvdslelem  16238  bitsinv1lem  16370  bitsshft  16404  smuval2  16411  smupvallem  16412  gcdcllem1  16428  bezoutlem2  16469  bezoutlem3  16470  algcvga  16508  isprm3  16612  isprm5  16636  oddprmdvds  16833  vdwlem13  16923  vdwnnlem1  16925  vdwnnlem3  16927  ramub1lem1  16956  prmgaplem5  16985  imasaddfnlem  17450  divsfval  17469  catpropd  17633  joindmss  18301  meetdmss  18315  psdmrn  18497  odlem1  19432  gexlem1  19476  cygctb  19789  rngisomring1  20371  lmodfopnelem1  20819  islss  20855  lspsneq0  20933  lspsneq  21047  psgnodpmr  21515  obselocv  21653  mvrf1  21911  evlseu  22006  mpfrcl  22008  ppttop  22910  epttop  22912  elcls  22976  restntr  23085  cnprest  23192  regsep  23237  nrmsep3  23258  lmmo  23283  cmpsublem  23302  cmpsub  23303  hauscmplem  23309  txcnpi  23511  txcnp  23523  fbun  23743  fbfinnfr  23744  trfbas2  23746  fgcl  23781  filssufilg  23814  ufinffr  23832  isfcls  23912  fclsrest  23927  flimfnfcls  23931  alexsubALTlem2  23951  alexsubALTlem3  23952  alexsubALTlem4  23953  alexsubALT  23954  cnextcn  23970  imasf1oxms  24393  metequiv2  24414  tngngpim  24563  iccpnfcnv  24858  iccpnfhmeo  24859  iscau2  25193  caun0  25197  minveclem3b  25344  itg1climres  25631  mbfi1fseqlem4  25635  ellimc3  25796  limccnp2  25809  dvlip  25914  itgsubstlem  25971  elply2  26117  coefv0  26169  coemulc  26176  ulmss  26322  sineq0  26449  scvxcvx  26912  sqf11  27065  ppiublem1  27129  fsumvma  27140  2sq2  27360  ostth  27566  sltres  27590  nosepdmlem  27611  nobdaymin  27705  nocvxminlem  27706  addsprop  27906  mptelee  28858  brbtwn2  28868  colinearalg  28873  axcontlem4  28930  upgrres1  29276  usgr2trlncl  29723  umgrclwwlkge2  29953  upgr4cycl4dv4e  30147  1to3vfriendship  30243  3cyclfrgrrn1  30247  n4cyclfrgr  30253  frgrncvvdeqlem8  30268  frgrwopreg  30285  2clwwlk2clwwlk  30312  numclwwlk2lem1  30338  frgrreg  30356  frgrogt3nreg  30359  nmcvcn  30657  chlimi  31196  ocsh  31245  shsvs  31285  h1datomi  31543  stcl  32178  stge0  32186  stle1  32187  stm1addi  32207  stm1add3i  32209  cvnsym  32252  mdbr2  32258  dmdbr2  32265  mdsl0  32272  mdsl1i  32283  mdsl2i  32284  cvmdi  32286  atexch  32343  atcvat4i  32359  cdj1i  32395  1arithufdlem4  33494  xrge0iifcnv  33899  esumpr2  34033  sigaclci  34098  cntmeas  34192  mbfmcnt  34235  ballotlemfc0  34460  ballotlemfcc  34461  bnj1379  34796  bnj607  34882  bnj908  34897  bnj938  34903  bnj1174  34969  bnj1280  34986  f1resrcmplf1dlem  35052  fnrelpredd  35055  axnulg  35058  tz9.1regs  35066  cusgr3cyclex  35108  loop1cycl  35109  acycgrislfgr  35124  pthacycspth  35129  iccllysconn  35222  satffunlem1lem1  35374  satfvel  35384  sate0fv0  35389  antnestlaw2  35664  funpsstri  35738  fundmpss  35739  dfon2lem3  35758  dfon2lem4  35759  dfon2lem6  35761  dfon2lem9  35764  dfon2  35765  hbimtg  35779  hbaltg  35780  dfrdg4  35924  btwntriv2  35985  btwncomim  35986  btwnswapid  35990  btwnexch3  35993  ifscgr  36017  lineunray  36120  hilbert1.2  36128  cldbnd  36299  tailfb  36350  meran3  36386  arg-ax  36389  ontopbas  36401  onsuct0  36414  limsucncmpi  36418  ordcmp  36420  onint1  36422  weiunpo  36438  bj-syl66ib  36528  bj-gl4  36568  bj-alexim  36600  bj-nfimt  36611  bj-ax6e  36641  bj-hbalt  36654  axc11n11r  36656  bj-nnfim  36719  bj-nnfan  36721  bj-nnfor  36723  bj-nnford  36724  bj-nnflemaa  36735  bj-nnflemae  36737  bj-19.21t  36742  bj-19.23t  36743  bj-19.42t  36746  bj-sbft  36748  bj-hbsb3t  36761  bj-cbv2hv  36770  bj-equsal1t  36795  bj-0int  37074  bj-bary1lem1  37284  topdifinffinlem  37320  isbasisrelowllem1  37328  isbasisrelowllem2  37329  iooelexlt  37335  finorwe  37355  finxpreclem1  37362  finxpreclem2  37363  isinf2  37378  fvineqsneu  37384  fvineqsneq  37385  pibt2  37390  wl-spae  37494  wl-19.8eqv  37496  wl-nfeqfb  37509  wl-mo3t  37549  wl-ax11-lem3  37560  fin2so  37586  poimirlem29  37628  poimirlem30  37629  poimirlem31  37630  poimirlem32  37631  ismblfin  37640  indexdom  37713  fzmul  37720  heibor1lem  37788  heibor  37800  exidu1  37835  rngoideu  37882  zerdivemp1x  37926  ispridl2  38017  cnf1dd  38069  cnf2dd  38070  cnfn1dd  38071  cnfn2dd  38072  orcomdd  38146  disjlem14  38775  disjdmqsss  38779  disjdmqscossss  38780  prtlem14  38852  prter2  38859  aev-o  38909  ax12eq  38919  ax12el  38920  ax12indn  38921  ax12indi  38922  lsatn0  38977  lsatcmp  38981  lsatcv0  39009  lfl1dim  39099  lfl1dim2N  39100  lkrss2N  39147  lub0N  39167  glb0N  39171  glbconxN  39357  hl2at  39384  cvrexchlem  39398  cvratlem  39400  cvrat4  39422  psubspi  39726  pointpsubN  39730  elpaddn0  39779  paddasslem17  39815  ispsubcl2N  39926  ldilval  40092  trlord  40548  diaelrnN  41024  cdlemm10N  41097  cdlemn11pre  41189  dihord2pre  41204  dihglblem2N  41273  dihglblem3N  41274  mapdrvallem2  41624  ioin9i8  42180  sn-sup2  42464  incssnn0  42684  fphpd  42789  rmxycomplete  42890  dford3lem1  42999  iocinico  43185  onsupnmax  43201  cantnfresb  43297  cantnf2  43298  tfsconcatb0  43317  tfsconcat0b  43319  sdomne0  43386  sdomne0d  43387  ensucne0OLD  43503  al3im  43620  brtrclfv2  43700  frege129d  43736  frege60a  43851  frege60c  43896  frege70  43906  rfovcnvf1od  43977  clsk1indlem3  44016  neik0pk1imk0  44020  gneispace  44107  gneispaceel2  44117  gneispacess2  44119  dvconstbi  44307  axc5c4c711toc7  44377  axc5c4c711to11  44378  pm14.24  44405  sbiota1  44407  bi33imp12  44465  bi123imp0  44470  ee233  44493  vk15.4j  44502  ssralv2  44505  alrim3con13v  44507  tratrb  44510  onfrALTlem3  44518  onfrALTlem2  44520  19.41rg  44524  hbimpg  44528  hbalg  44529  ax6e2ndeq  44533  e2  44605  ee223  44608  sspwtrALT  44795  sspwtrALT2  44796  suctrALT2  44810  trintALT  44854  isosctrlem1ALT  44907  relpmin  44926  traxext  44951  modelaxreplem2  44953  ssclaxsep  44956  fnchoice  45007  mptfnd  45220  stoweidlem62  46044  2reu8i  47098  2reuimp  47100  ffnafv  47156  lswn0  47429  reupr  47507  reuopreuprim  47511  requad2  47608  bgoldbnnsum3prm  47789  bgoldbtbndlem2  47791  bgoldbtbndlem4  47793  gricsym  47905  gpgedgvtx1  48037  ply1mulgsumlem2  48360  iunord  49649  setrec2fun  49665