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  205  imbitrdi  253  imbitrrdi  254  biimtrdi  255  biimtrrdi  256  jaoi  866  pm2.37  981  pm2.81  982  oplem1  1065  3jao  1440  impsingle  1641  al2im  1828  exlimdv  1947  19.23v  1956  spimfw  1979  ax13b  2046  nf5-1  2173  hbald  2196  19.8a  2210  spimedv  2226  19.9d  2232  sbequ1  2277  sbft  2298  cbv2w  2362  spimed  2413  cbv2  2428  cbv2h  2431  ax12  2448  axc11n  2451  equvini  2480  sb2  2504  sb4a  2505  mo3  2585  mopick  2646  moexexlem  2647  dvelimdc  2942  necon1ad  2968  necon4bd  2971  rsp2  3273  mo2icl  3671  2reu1  3845  reuss2  4273  reupick2  4278  elpwunsn  4637  pwpw0  4765  sssn  4778  iuneqconst  4955  disjiun  5082  trun  5212  reusv1  5348  reusv3i  5355  ralxfrALT  5366  exneq  5397  opth1  5437  copsexgwOLD  5453  copsexg  5454  opelopabt  5496  solin  5575  wefrc  5634  frinxp  5723  ssrelrn  5863  dmcosseq  5947  dmcosseqOLD  5948  reuop  6269  ordunidif  6385  oneqmini  6388  suctr  6423  ordsssuc2  6428  iotan0  6500  fv3  6874  ndmfv  6888  ssimaex  6941  fvopab3ig  6960  iinpreima  7039  fvcofneq  7063  dff3  7070  dff4  7071  ffnfv  7089  fnsnr  7136  fprb  7167  elunirn  7224  f1mpt  7234  isomin  7310  oprabidw  7416  oprabid  7417  mpoeq123  7457  sorpsscmpl  7706  dfwe2  7746  ssorduni  7751  ssonprc  7759  nlimsucg  7811  ordunisuc2  7813  tfinds  7829  ssnlim  7855  f1oweALT  7942  mptcnfimad  7956  el2mpocl  8053  f1o2ndf1  8089  frxp  8094  soxp  8097  poxp2  8111  poxp3  8118  poseq  8126  brtpos  8203  rntpos  8207  dftpos4  8213  onfununi  8300  onnseq  8303  smores2  8313  smo11  8323  tfr3  8358  rdglim2  8391  tz7.48lem  8400  tz7.49  8404  seqomlem2  8410  oawordex  8514  oa00  8516  oaass  8518  om00  8532  odi  8536  omass  8537  oeordi  8545  oelim2  8553  omsmo  8616  eroveu  8782  eceqoveq  8792  map0g  8855  fundmen  9001  sdomdif  9086  onsdominel  9087  pssnn  9126  nneneq  9163  php3  9166  f1finf1o  9206  findcard3  9216  unblem1  9225  fiint  9260  ixpfi2  9283  dffi2  9359  elfiun  9366  fisup2g  9405  fiinf2g  9438  wemaplem2  9485  elirrv  9535  elirrvOLD  9536  preleqALT  9562  inf3lem2  9574  inf3lem3  9575  inf3lem6  9578  noinfep  9605  epfrs  9676  tcmin  9684  r1sdom  9722  tz9.12lem3  9737  rankelb  9772  bndrank  9789  rankunb  9798  rankuni2b  9801  cplem1  9837  karden  9843  carduni  9929  infxpenlem  9959  dfac8alem  9975  alephdom  10027  cardinfima  10043  alephval3  10056  dfac5lem4  10072  dfac5lem5  10073  dfac5lem4OLD  10074  dfac5  10075  dfac2b  10077  kmlem13  10109  nnadju  10144  ackbij1b  10184  cfub  10195  coflim  10208  cflim2  10210  cfslbn  10214  cfslb2n  10215  cofsmo  10216  cfsmolem  10217  sornom  10224  fincssdom  10270  isf32lem1  10300  isf32lem2  10301  isf32lem9  10308  isf34lem4  10324  isfin1-3  10333  axcc4  10386  domtriomlem  10389  axdc2lem  10395  axdc3lem2  10398  zorn2lem4  10446  zorn2lem6  10448  zornn0g  10452  uniimadom  10491  cardmin  10511  ficard  10512  konigthlem  10516  alephreg  10530  cfpwsdom  10532  axextnd  10539  fpwwe2lem5  10583  fpwwe2lem11  10589  fpwwe2lem12  10590  fpwwe2  10591  canthp1lem2  10601  gchpwdom  10618  winalim2  10644  tskuni  10731  grupr  10745  grur1a  10767  axgroth6  10776  grothomex  10777  eltskm  10791  addclpi  10840  nqereu  10877  ltexnq  10923  nsmallnq  10925  genpn0  10951  genpss  10952  genpnmax  10955  ltaddpr  10982  reclem3pr  10997  reclem4pr  10998  suplem1pr  11000  supsrlem  11059  1re  11171  dedekindle  11337  addrid  11353  negn0  11606  negf1o  11607  negfi  12131  sup2  12138  supadd  12150  supmullem1  12152  supmullem2  12153  zmulcl  12610  zeo  12649  uz11  12854  uzwo  12902  eqreznegel  12925  lbzbi  12927  qextlt  13196  qextle  13197  xrsupsslem  13300  xrinfmsslem  13301  supxrun  13309  supxrpnf  13311  supxrunb1  13312  supxrunb2  13313  fzm1  13602  uzrdgfni  13961  hasheqf1oi  14354  hashreshashfun  14442  leisorel  14463  fundmge2nop0  14505  wrdsymb0  14552  swrdnnn0nd  14660  swrdccatin2d  14747  cshinj  14814  repswcshw  14815  rennim  15242  01sqrexlem6  15250  caubnd  15362  sqreulem  15363  caucvgrlem  15676  fsumcvg  15715  supcvg  15862  prodeq2ii  15917  fprodcvg  15936  prodmo  15942  dvdslelem  16319  bitsinv1lem  16451  bitsshft  16485  smuval2  16492  smupvallem  16493  gcdcllem1  16509  bezoutlem2  16550  bezoutlem3  16551  algcvga  16589  isprm3  16693  isprm5  16718  oddprmdvds  16915  vdwlem13  17005  vdwnnlem1  17007  vdwnnlem3  17009  ramub1lem1  17038  prmgaplem5  17067  imasaddfnlem  17534  divsfval  17553  catpropd  17717  joindmss  18385  meetdmss  18399  psdmrn  18581  odlem1  19551  gexlem1  19595  cygctb  19908  rngisomring1  20489  lmodfopnelem1  20938  islss  20974  lspsneq0  21052  lspsneq  21165  psgnodpmr  21615  obselocv  21753  mvrf1  22010  evlseu  22109  mpfrcl  22111  ppttop  23040  epttop  23042  elcls  23106  restntr  23215  cnprest  23322  regsep  23367  nrmsep3  23388  lmmo  23413  cmpsublem  23432  cmpsub  23433  hauscmplem  23439  txcnpi  23641  txcnp  23653  fbun  23873  fbfinnfr  23874  trfbas2  23876  fgcl  23911  filssufilg  23944  ufinffr  23962  isfcls  24042  fclsrest  24057  flimfnfcls  24061  alexsubALTlem2  24081  alexsubALTlem3  24082  alexsubALTlem4  24083  alexsubALT  24084  cnextcn  24100  imasf1oxms  24522  metequiv2  24543  tngngpim  24692  iccpnfcnv  24979  iccpnfhmeo  24980  iscau2  25312  caun0  25316  minveclem3b  25463  itg1climres  25749  mbfi1fseqlem4  25753  ellimc3  25914  limccnp2  25927  dvlip  26028  itgsubstlem  26083  elply2  26229  coefv0  26281  coemulc  26288  ulmss  26430  sineq0  26559  scvxcvx  27020  sqf11  27173  ppiublem1  27236  fsumvma  27247  2sq2  27467  ostth  27673  ltsres  27696  nosepdmlem  27717  nobdaymin  27816  nocvxminlem  27817  addsprop  28039  mpteleeOLD  29035  brbtwn2  29045  colinearalg  29050  axcontlem4  29107  upgrres1  29453  usgr2trlncl  29899  umgrclwwlkge2  30132  upgr4cycl4dv4e  30326  1to3vfriendship  30422  3cyclfrgrrn1  30426  n4cyclfrgr  30432  frgrncvvdeqlem8  30447  frgrwopreg  30464  2clwwlk2clwwlk  30491  numclwwlk2lem1  30517  frgrreg  30535  frgrogt3nreg  30538  nmcvcn  30837  chlimi  31376  ocsh  31425  shsvs  31465  h1datomi  31723  stcl  32358  stge0  32366  stle1  32367  stm1addi  32387  stm1add3i  32389  cvnsym  32432  mdbr2  32438  dmdbr2  32445  mdsl0  32452  mdsl1i  32463  mdsl2i  32464  cvmdi  32466  atexch  32523  atcvat4i  32539  cdj1i  32575  1arithufdlem4  33697  xrge0iifcnv  34184  esumpr2  34318  sigaclci  34383  cntmeas  34477  mbfmcnt  34519  ballotlemfc0  34744  ballotlemfcc  34745  bnj1379  35082  bnj607  35168  bnj908  35183  bnj938  35189  bnj1174  35255  bnj1280  35272  f1resrcmplf1dlem  35337  fnrelpredd  35342  r1filimi  35354  fineqvinfep  35376  tz9.1regs  35385  axsepg2  35391  axsepg4  35394  axnulg  35396  axpowg2  35398  axpowg3  35399  cusgr3cyclex  35434  loop1cycl  35435  acycgrislfgr  35450  pthacycspth  35455  iccllysconn  35548  satffunlem1lem1  35700  satfvel  35710  sate0fv0  35715  antnestlaw2  35990  funpsstri  36064  fundmpss  36065  dfon2lem3  36081  dfon2lem4  36082  dfon2lem6  36084  dfon2lem9  36087  dfon2  36088  hbimtg  36102  hbaltg  36103  dfrdg4  36249  btwntriv2  36310  btwncomim  36311  btwnswapid  36315  btwnexch3  36318  ifscgr  36342  lineunray  36445  hilbert1.2  36453  cldbnd  36634  tailfb  36685  meran3  36721  arg-ax  36724  ontopbas  36736  onsuct0  36749  limsucncmpi  36753  ordcmp  36755  onint1  36757  weiunpo  36773  axtcond  36786  axuntco  36787  dfttc4lem2  36837  bj-bisimpl  36943  bj-bisimpr  36944  bj-syl66ib  36945  bj-gl4  36986  bj-alexim  37031  bj-nfimt  37043  bj-spvw  37055  bj-cbvalvv  37059  bj-ax6e  37088  bj-hbald  37102  axc11n11r  37106  bj-nnfim  37175  bj-nnfan  37177  bj-nnfor  37179  bj-nnford  37180  bj-19.21t  37184  bj-19.23t  37185  bj-19.42t  37188  bj-sbft  37201  bj-nnflemaa  37209  bj-nnflemae  37211  bj-hbsb3t  37221  bj-cbv2hv  37230  bj-equsal1t  37255  bj-axreprepsep  37508  bj-0int  37539  bj-bary1lem1  37751  topdifinffinlem  37789  isbasisrelowllem1  37797  isbasisrelowllem2  37798  iooelexlt  37804  finorwe  37824  finxpreclem1  37831  finxpreclem2  37832  isinf2  37847  fvineqsneu  37853  fvineqsneq  37854  pibt2  37859  wl-spae  37972  wl-19.8eqv  37974  wl-nfeqfb  37987  wl-mo3t  38027  wl-eujustlem1  38039  fin2so  38054  poimirlem29  38096  poimirlem30  38097  poimirlem31  38098  poimirlem32  38099  ismblfin  38108  indexdom  38181  fzmul  38188  heibor1lem  38256  heibor  38268  exidu1  38303  rngoideu  38350  zerdivemp1x  38394  ispridl2  38485  cnf1dd  38537  cnf2dd  38538  cnfn1dd  38539  cnfn2dd  38540  orcomdd  38614  disjlem14  39348  disjdmqsss  39352  disjdmqscossss  39353  prtlem14  39446  prter2  39453  aev-o  39503  ax12eq  39513  ax12el  39514  ax12indn  39515  ax12indi  39516  lsatn0  39571  lsatcmp  39575  lsatcv0  39603  lfl1dim  39693  lfl1dim2N  39694  lkrss2N  39741  lub0N  39761  glb0N  39765  glbconxN  39950  hl2at  39977  cvrexchlem  39991  cvratlem  39993  cvrat4  40015  psubspi  40319  pointpsubN  40323  elpaddn0  40372  paddasslem17  40408  ispsubcl2N  40519  ldilval  40685  trlord  41141  diaelrnN  41617  cdlemm10N  41690  cdlemn11pre  41782  dihord2pre  41797  dihglblem2N  41866  dihglblem3N  41867  mapdrvallem2  42217  ioin9i8  42772  sn-sup2  43061  incssnn0  43240  fphpd  43341  rmxycomplete  43442  dford3lem1  43551  iocinico  43737  onsupnmax  43753  cantnfresb  43849  cantnf2  43850  tfsconcatb0  43869  tfsconcat0b  43871  sdomne0  43937  sdomne0d  43938  ensucne0OLD  44054  al3im  44171  brtrclfv2  44251  frege129d  44287  frege60a  44402  frege60c  44447  frege70  44457  rfovcnvf1od  44528  clsk1indlem3  44567  neik0pk1imk0  44571  gneispace  44658  gneispaceel2  44668  gneispacess2  44670  dvconstbi  44858  axc5c4c711toc7  44928  axc5c4c711to11  44929  pm14.24  44956  sbiota1  44958  bi33imp12  45015  bi123imp0  45020  ee233  45043  vk15.4j  45052  ssralv2  45055  alrim3con13v  45057  tratrb  45060  onfrALTlem3  45068  onfrALTlem2  45070  19.41rg  45074  hbimpg  45078  hbalg  45079  ax6e2ndeq  45083  e2  45155  ee223  45158  sspwtrALT  45345  sspwtrALT2  45346  suctrALT2  45360  trintALT  45404  isosctrlem1ALT  45457  relpmin  45476  traxext  45501  modelaxreplem2  45503  ssclaxsep  45506  fnchoice  45557  mptfnd  45765  stoweidlem62  46584  2reu8i  47655  2reuimp  47657  ffnafv  47713  lswn0  47998  reupr  48076  reuopreuprim  48080  requad2  48193  bgoldbnnsum3prm  48374  bgoldbtbndlem2  48376  bgoldbtbndlem4  48378  gricsym  48491  gpgedgvtx1  48632  ply1mulgsumlem2  48957  iunord  50245  setrec2fun  50261