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  166  looinv  204  syl6ib  252  syl6ibr  253  syl6bi  254  syl6bir  255  jaoi  852  pm2.37  965  pm2.81  966  oplem1  1049  3jao  1418  impsingle  1609  al2im  1796  exlimdv  1911  19.23v  1920  19.36imv  1923  spimfw  1945  ax13b  2016  nf5-1  2116  hbald  2139  19.8a  2144  spimedv  2162  19.9d  2168  sbequ1  2213  sbft  2233  19.9ht  2302  spimed  2362  cbv2  2379  cbv2h  2382  axc15OLD  2401  ax12  2402  axc11n  2405  equvini  2434  equviniOLD  2435  sb2  2458  sb4a  2463  sbequiOLD  2488  sbi1OLD  2496  dfsb2ALT  2545  sbftALT  2547  sbequiALT  2550  hbsb2ALT  2553  sbi1ALT  2560  mo3  2604  mo3OLD  2605  mopick  2680  moexexlem  2681  dvelimdc  2973  necon1ad  3001  necon4bd  3004  rsp2  3180  vtoclgft  3496  mo2icl  3641  2reu1  3809  reuss2  4203  reupick2  4209  elpwunsn  4528  pwpw0  4653  sssn  4666  pwsnALT  4738  dfiun2gOLD  4859  disjiun  4950  reusv1  5189  reusv3i  5196  ralxfrALT  5207  opth1  5259  copsexg  5273  opelopabt  5309  wefrc  5437  frinxp  5520  ssrelrn  5649  reuop  6019  ordunidif  6114  oneqmini  6117  suctr  6149  ordsssuc2  6154  fv3  6556  ndmfv  6568  ssimaex  6615  fvopab3ig  6631  iinpreima  6702  fvcofneq  6724  dff3  6729  dff4  6730  ffnfv  6745  fnsnr  6790  fprb  6823  elunirn  6875  f1mpt  6884  isomin  6953  oprabid  7047  mpoeq123  7084  sorpsscmpl  7318  dfwe2  7352  ssorduni  7356  ssonprc  7363  nlimsucg  7413  ordunisuc2  7415  tfinds  7430  ssnlim  7455  fiun  7500  f1oweALT  7529  el2mpocl  7637  f1o2ndf1  7671  frxp  7673  soxp  7676  brtpos  7752  rntpos  7756  dftpos4  7762  onfununi  7830  onnseq  7833  smores2  7843  smo11  7853  tfr3  7887  rdglim2  7920  tz7.48lem  7928  tz7.49  7932  seqomlem2  7938  oawordex  8033  oa00  8035  oaass  8037  om00  8051  odi  8055  omass  8056  oeordi  8063  oelim2  8071  omsmo  8131  eroveu  8242  eceqoveq  8252  map0g  8298  fundmen  8431  sdomdif  8512  onsdominel  8513  nneneq  8547  php3  8550  onomeneq  8554  pssnn  8582  f1finf1o  8591  findcard3  8607  unblem1  8616  fiint  8641  ixpfi2  8668  dffi2  8733  elfiun  8740  fisup2g  8778  fiinf2g  8810  wemaplem2  8857  preleqALT  8926  inf3lem2  8938  inf3lem3  8939  inf3lem6  8942  noinfep  8969  epfrs  9019  tcmin  9029  r1sdom  9049  tz9.12lem3  9064  rankelb  9099  bndrank  9116  rankunb  9125  rankuni2b  9128  cplem1  9164  karden  9170  carduni  9256  infxpenlem  9285  dfac8alem  9301  alephdom  9353  cardinfima  9369  alephval3  9382  dfac5lem4  9398  dfac5lem5  9399  dfac5  9400  dfac2b  9402  kmlem13  9434  ackbij1b  9507  cfub  9517  coflim  9529  cflim2  9531  cfslbn  9535  cfslb2n  9536  cofsmo  9537  cfsmolem  9538  sornom  9545  fincssdom  9591  isf32lem1  9621  isf32lem2  9622  isf32lem9  9629  isf34lem4  9645  isfin1-3  9654  axcc4  9707  domtriomlem  9710  axdc2lem  9716  axdc3lem2  9719  zorn2lem4  9767  zorn2lem6  9769  zornn0g  9773  axdclem2  9788  uniimadom  9812  cardmin  9832  ficard  9833  konigthlem  9836  alephreg  9850  cfpwsdom  9852  axextnd  9859  fpwwe2lem6  9903  fpwwe2lem12  9909  fpwwe2lem13  9910  fpwwe2  9911  canthp1lem2  9921  gchpwdom  9938  winalim2  9964  tskuni  10051  grupr  10065  grur1a  10087  axgroth6  10096  grothomex  10097  eltskm  10111  addclpi  10160  nqereu  10197  ltexnq  10243  nsmallnq  10245  genpn0  10271  genpss  10272  genpnmax  10275  ltaddpr  10302  reclem3pr  10317  reclem4pr  10318  suplem1pr  10320  supsrlem  10379  1re  10487  dedekindle  10651  addid1  10667  negn0  10917  negf1o  10918  negfi  11437  fiminreOLD  11438  sup2  11445  supadd  11457  supmullem1  11459  supmullem2  11460  zmulcl  11880  zeo  11917  uz11  12116  uzwo  12160  eqreznegel  12183  lbzbi  12185  qextlt  12446  qextle  12447  xrsupsslem  12550  xrinfmsslem  12551  supxrun  12559  supxrpnf  12561  supxrunb1  12562  supxrunb2  12563  fzm1  12837  uzrdgfni  13176  hasheqf1oi  13562  hashreshashfun  13648  leisorel  13666  fundmge2nop0  13696  wrdsymb0  13747  swrdnnn0nd  13854  swrdccatin2d  13942  cshinj  14009  repswcshw  14010  rennim  14432  sqrlem6  14441  caubnd  14552  sqreulem  14553  caucvgrlem  14863  fsumcvg  14902  supcvg  15044  prodeq2ii  15100  fprodcvg  15117  prodmo  15123  dvdslelem  15492  bitsinv1lem  15623  bitsshft  15657  smuval2  15664  smupvallem  15665  gcdcllem1  15681  bezoutlem2  15717  bezoutlem3  15718  algcvga  15752  isprm3  15856  isprm5  15880  oddprmdvds  16068  vdwlem13  16158  vdwnnlem1  16160  vdwnnlem3  16162  ramub1lem1  16191  prmgaplem5  16220  imasaddfnlem  16630  divsfval  16649  catpropd  16808  joindmss  17446  meetdmss  17460  psdmrn  17646  odlem1  18394  gexlem1  18434  cygctb  18733  lmodfopnelem1  19360  islss  19396  lspsneq0  19474  lspsneq  19584  mvrf1  19893  evlseu  19983  mpfrcl  19985  psgnodpmr  20416  obselocv  20554  ppttop  21299  epttop  21301  elcls  21365  restntr  21474  cnprest  21581  regsep  21626  nrmsep3  21647  lmmo  21672  cmpsublem  21691  cmpsub  21692  hauscmplem  21698  txcnpi  21900  txcnp  21912  fbun  22132  fbfinnfr  22133  trfbas2  22135  fgcl  22170  filssufilg  22203  ufinffr  22221  isfcls  22301  fclsrest  22316  flimfnfcls  22320  alexsubALTlem2  22340  alexsubALTlem3  22341  alexsubALTlem4  22342  alexsubALT  22343  cnextcn  22359  imasf1oxms  22782  metequiv2  22803  tngngpim  22951  iccpnfcnv  23231  iccpnfhmeo  23232  iscau2  23563  caun0  23567  minveclem3b  23714  itg1climres  23998  mbfi1fseqlem4  24002  ellimc3  24160  limccnp2  24173  dvlip  24273  itgsubstlem  24328  elply2  24469  coefv0  24521  coemulc  24528  ulmss  24668  sineq0  24792  scvxcvx  25245  sqf11  25398  ppiublem1  25460  fsumvma  25471  2sq2  25691  ostth  25897  mptelee  26364  brbtwn2  26374  colinearalg  26379  axcontlem4  26436  upgrres1  26778  usgr2trlncl  27228  umgrclwwlkge2  27456  upgr4cycl4dv4e  27651  1to3vfriendship  27752  3cyclfrgrrn1  27756  n4cyclfrgr  27762  frgrncvvdeqlem8  27777  frgrwopreg  27794  2clwwlk2clwwlk  27821  numclwwlk2lem1  27847  frgrreg  27865  frgrogt3nreg  27868  nmcvcn  28163  chlimi  28702  ocsh  28751  shsvs  28791  h1datomi  29049  stcl  29684  stge0  29692  stle1  29693  stm1addi  29713  stm1add3i  29715  cvnsym  29758  mdbr2  29764  dmdbr2  29771  mdsl0  29778  mdsl1i  29789  mdsl2i  29790  cvmdi  29792  atexch  29849  atcvat4i  29865  cdj1i  29901  xrge0iifcnv  30793  esumpr2  30943  sigaclci  31008  cntmeas  31102  mbfmcnt  31143  ballotlemfc0  31367  ballotlemfcc  31368  bnj1379  31719  bnj607  31804  bnj908  31819  bnj938  31825  bnj1174  31889  bnj1280  31906  f1resrcmplf1dlem  31973  cusgr3cyclex  31991  loop1cycl  31992  acycgrislfgr  32007  pthacycspth  32012  iccllysconn  32105  satffunlem1lem1  32257  satfvel  32267  sate0fv0  32272  funpsstri  32616  fundmpss  32617  dfon2lem3  32638  dfon2lem4  32639  dfon2lem6  32641  dfon2lem9  32644  dfon2  32645  hbimtg  32660  hbaltg  32661  dftrpred3g  32681  poseq  32704  sltres  32778  nosepdmlem  32796  nocvxminlem  32856  nocvxmin  32857  dfrdg4  33021  btwntriv2  33082  btwncomim  33083  btwnswapid  33087  btwnexch3  33090  ifscgr  33114  lineunray  33217  hilbert1.2  33225  cldbnd  33283  tailfb  33334  meran3  33370  arg-ax  33373  ontopbas  33385  onsuct0  33398  limsucncmpi  33402  ordcmp  33404  onint1  33406  bj-syl66ib  33496  bj-gl4  33535  bj-alexim  33561  bj-nfimt  33573  bj-ax6e  33600  bj-hbalt  33614  axc11n11r  33616  bj-hbsb3t  33654  bj-cbv2hv  33664  bj-equsal1t  33715  bj-nnfim  33859  bj-nnfant  33860  bj-nnfand  33861  bj-nnfort  33862  bj-nnflemaa  33873  bj-nnflemae  33875  bj-sbft  33879  bj-0int  33992  bj-bary1lem1  34129  topdifinffinlem  34159  isbasisrelowllem1  34167  isbasisrelowllem2  34168  iooelexlt  34174  finorwe  34194  finxpreclem1  34201  finxpreclem2  34202  isinf2  34217  fvineqsneu  34223  fvineqsneq  34224  pibt2  34229  wl-spae  34294  wl-19.8eqv  34296  wl-nfeqfb  34308  wl-mo3t  34343  wl-ax11-lem3  34350  fin2so  34410  poimirlem29  34452  poimirlem30  34453  poimirlem31  34454  poimirlem32  34455  ismblfin  34464  indexdom  34541  fzmul  34548  heibor1lem  34619  heibor  34631  exidu1  34666  rngoideu  34713  zerdivemp1x  34757  ispridl2  34848  cnf1dd  34900  cnf2dd  34901  cnfn1dd  34902  cnfn2dd  34903  orcomdd  34977  prtlem14  35541  prter2  35548  aev-o  35598  ax12eq  35608  ax12el  35609  ax12indn  35610  ax12indi  35611  lsatn0  35666  lsatcmp  35670  lsatcv0  35698  lfl1dim  35788  lfl1dim2N  35789  lkrss2N  35836  lub0N  35856  glb0N  35860  glbconxN  36045  hl2at  36072  cvrexchlem  36086  cvratlem  36088  cvrat4  36110  psubspi  36414  pointpsubN  36418  elpaddn0  36467  paddasslem17  36503  ispsubcl2N  36614  ldilval  36780  trlord  37236  diaelrnN  37712  cdlemm10N  37785  cdlemn11pre  37877  dihord2pre  37892  dihglblem2N  37961  dihglblem3N  37962  mapdrvallem2  38312  ioin9i8  38629  sn-dtru  38641  incssnn0  38793  fphpd  38898  rmxycomplete  38999  dford3lem1  39108  iocinico  39303  ensucne0OLD  39381  al3im  39476  brtrclfv2  39557  frege129d  39593  frege60a  39709  frege60c  39754  frege70  39764  rfovcnvf1od  39835  clsk1indlem3  39878  neik0pk1imk0  39882  gneispace  39969  gneispaceel2  39979  gneispacess2  39981  dvconstbi  40204  axc5c4c711toc7  40274  axc5c4c711to11  40275  pm14.24  40302  sbiota1  40304  bi33imp12  40363  bi123imp0  40369  ee233  40392  vk15.4j  40401  ssralv2  40404  alrim3con13v  40406  tratrb  40409  onfrALTlem3  40417  onfrALTlem2  40419  19.41rg  40423  hbimpg  40427  hbalg  40428  ax6e2ndeq  40432  e2  40504  ee223  40507  sspwtrALT  40695  sspwtrALT2  40696  suctrALT2  40710  trintALT  40754  isosctrlem1ALT  40807  fnchoice  40825  mptfnd  41053  stoweidlem62  41889  2reu8i  42828  2reuimp  42830  ffnafv  42886  lswn0  43086  reupr  43166  reuopreuprim  43170  requad2  43270  bgoldbnnsum3prm  43451  bgoldbtbndlem2  43453  bgoldbtbndlem4  43455  ply1mulgsumlem2  43921  iunord  44259  setrec2fun  44275