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  3254  mo2icl  3685  2reu1  3860  reuss2  4289  reupick2  4294  elpwunsn  4648  pwpw0  4777  sssn  4790  iuneqconst  4967  disjiun  5095  reusv1  5352  reusv3i  5359  ralxfrALT  5370  exneq  5395  opth1  5435  copsexgw  5450  copsexg  5451  opelopabt  5492  solin  5573  wefrc  5632  frinxp  5721  ssrelrn  5858  dmcosseq  5940  reuop  6266  ordunidif  6382  oneqmini  6385  suctr  6420  ordsssuc2  6425  iotan0  6501  fv3  6876  ndmfv  6893  ssimaex  6946  fvopab3ig  6964  iinpreima  7041  fvcofneq  7065  dff3  7072  dff4  7073  ffnfv  7091  fnsnr  7137  fprb  7168  elunirn  7225  f1mpt  7236  isomin  7312  oprabidw  7418  oprabid  7419  mpoeq123  7461  sorpsscmpl  7710  dfwe2  7750  ssorduni  7755  ssonprc  7763  nlimsucg  7818  ordunisuc2  7820  tfinds  7836  ssnlim  7862  f1oweALT  7951  mptcnfimad  7965  el2mpocl  8065  f1o2ndf1  8101  frxp  8105  soxp  8108  poxp2  8122  poxp3  8129  poseq  8137  brtpos  8214  rntpos  8218  dftpos4  8224  onfununi  8310  onnseq  8313  smores2  8323  smo11  8333  tfr3  8367  rdglim2  8400  tz7.48lem  8409  tz7.49  8413  seqomlem2  8419  oawordex  8521  oa00  8523  oaass  8525  om00  8539  odi  8543  omass  8544  oeordi  8551  oelim2  8559  omsmo  8622  eroveu  8785  eceqoveq  8795  map0g  8857  fundmen  9002  sdomdif  9089  onsdominel  9090  pssnn  9132  nneneq  9170  php3  9173  f1finf1o  9216  f1finf1oOLD  9217  findcard3  9229  findcard3OLD  9230  unblem1  9239  fiint  9277  fiintOLD  9278  ixpfi2  9301  dffi2  9374  elfiun  9381  fisup2g  9420  fiinf2g  9453  wemaplem2  9500  preleqALT  9570  inf3lem2  9582  inf3lem3  9583  inf3lem6  9586  noinfep  9613  epfrs  9684  tcmin  9694  r1sdom  9727  tz9.12lem3  9742  rankelb  9777  bndrank  9794  rankunb  9803  rankuni2b  9806  cplem1  9842  karden  9848  carduni  9934  infxpenlem  9966  dfac8alem  9982  alephdom  10034  cardinfima  10050  alephval3  10063  dfac5lem4  10079  dfac5lem5  10080  dfac5lem4OLD  10081  dfac5  10082  dfac2b  10084  kmlem13  10116  nnadju  10151  ackbij1b  10191  cfub  10202  coflim  10214  cflim2  10216  cfslbn  10220  cfslb2n  10221  cofsmo  10222  cfsmolem  10223  sornom  10230  fincssdom  10276  isf32lem1  10306  isf32lem2  10307  isf32lem9  10314  isf34lem4  10330  isfin1-3  10339  axcc4  10392  domtriomlem  10395  axdc2lem  10401  axdc3lem2  10404  zorn2lem4  10452  zorn2lem6  10454  zornn0g  10458  uniimadom  10497  cardmin  10517  ficard  10518  konigthlem  10521  alephreg  10535  cfpwsdom  10537  axextnd  10544  fpwwe2lem5  10588  fpwwe2lem11  10594  fpwwe2lem12  10595  fpwwe2  10596  canthp1lem2  10606  gchpwdom  10623  winalim2  10649  tskuni  10736  grupr  10750  grur1a  10772  axgroth6  10781  grothomex  10782  eltskm  10796  addclpi  10845  nqereu  10882  ltexnq  10928  nsmallnq  10930  genpn0  10956  genpss  10957  genpnmax  10960  ltaddpr  10987  reclem3pr  11002  reclem4pr  11003  suplem1pr  11005  supsrlem  11064  1re  11174  dedekindle  11338  addrid  11354  negn0  11607  negf1o  11608  negfi  12132  sup2  12139  supadd  12151  supmullem1  12153  supmullem2  12154  zmulcl  12582  zeo  12620  uz11  12818  uzwo  12870  eqreznegel  12893  lbzbi  12895  qextlt  13163  qextle  13164  xrsupsslem  13267  xrinfmsslem  13268  supxrun  13276  supxrpnf  13278  supxrunb1  13279  supxrunb2  13280  fzm1  13568  uzrdgfni  13923  hasheqf1oi  14316  hashreshashfun  14404  leisorel  14425  fundmge2nop0  14467  wrdsymb0  14514  swrdnnn0nd  14621  swrdccatin2d  14709  cshinj  14776  repswcshw  14777  rennim  15205  01sqrexlem6  15213  caubnd  15325  sqreulem  15326  caucvgrlem  15639  fsumcvg  15678  supcvg  15822  prodeq2ii  15877  fprodcvg  15896  prodmo  15902  dvdslelem  16279  bitsinv1lem  16411  bitsshft  16445  smuval2  16452  smupvallem  16453  gcdcllem1  16469  bezoutlem2  16510  bezoutlem3  16511  algcvga  16549  isprm3  16653  isprm5  16677  oddprmdvds  16874  vdwlem13  16964  vdwnnlem1  16966  vdwnnlem3  16968  ramub1lem1  16997  prmgaplem5  17026  imasaddfnlem  17491  divsfval  17510  catpropd  17670  joindmss  18338  meetdmss  18352  psdmrn  18532  odlem1  19465  gexlem1  19509  cygctb  19822  rngisomring1  20377  lmodfopnelem1  20804  islss  20840  lspsneq0  20918  lspsneq  21032  psgnodpmr  21499  obselocv  21637  mvrf1  21895  evlseu  21990  mpfrcl  21992  ppttop  22894  epttop  22896  elcls  22960  restntr  23069  cnprest  23176  regsep  23221  nrmsep3  23242  lmmo  23267  cmpsublem  23286  cmpsub  23287  hauscmplem  23293  txcnpi  23495  txcnp  23507  fbun  23727  fbfinnfr  23728  trfbas2  23730  fgcl  23765  filssufilg  23798  ufinffr  23816  isfcls  23896  fclsrest  23911  flimfnfcls  23915  alexsubALTlem2  23935  alexsubALTlem3  23936  alexsubALTlem4  23937  alexsubALT  23938  cnextcn  23954  imasf1oxms  24377  metequiv2  24398  tngngpim  24547  iccpnfcnv  24842  iccpnfhmeo  24843  iscau2  25177  caun0  25181  minveclem3b  25328  itg1climres  25615  mbfi1fseqlem4  25619  ellimc3  25780  limccnp2  25793  dvlip  25898  itgsubstlem  25955  elply2  26101  coefv0  26153  coemulc  26160  ulmss  26306  sineq0  26433  scvxcvx  26896  sqf11  27049  ppiublem1  27113  fsumvma  27124  2sq2  27344  ostth  27550  sltres  27574  nosepdmlem  27595  nocvxminlem  27689  nocvxmin  27690  addsprop  27883  mptelee  28822  brbtwn2  28832  colinearalg  28837  axcontlem4  28894  upgrres1  29240  usgr2trlncl  29690  umgrclwwlkge2  29920  upgr4cycl4dv4e  30114  1to3vfriendship  30210  3cyclfrgrrn1  30214  n4cyclfrgr  30220  frgrncvvdeqlem8  30235  frgrwopreg  30252  2clwwlk2clwwlk  30279  numclwwlk2lem1  30305  frgrreg  30323  frgrogt3nreg  30326  nmcvcn  30624  chlimi  31163  ocsh  31212  shsvs  31252  h1datomi  31510  stcl  32145  stge0  32153  stle1  32154  stm1addi  32174  stm1add3i  32176  cvnsym  32219  mdbr2  32225  dmdbr2  32232  mdsl0  32239  mdsl1i  32250  mdsl2i  32251  cvmdi  32253  atexch  32310  atcvat4i  32326  cdj1i  32362  1arithufdlem4  33518  xrge0iifcnv  33923  esumpr2  34057  sigaclci  34122  cntmeas  34216  mbfmcnt  34259  ballotlemfc0  34484  ballotlemfcc  34485  bnj1379  34820  bnj607  34906  bnj908  34921  bnj938  34927  bnj1174  34993  bnj1280  35010  f1resrcmplf1dlem  35076  fnrelpredd  35079  axnulg  35082  cusgr3cyclex  35123  loop1cycl  35124  acycgrislfgr  35139  pthacycspth  35144  iccllysconn  35237  satffunlem1lem1  35389  satfvel  35399  sate0fv0  35404  antnestlaw2  35679  funpsstri  35753  fundmpss  35754  dfon2lem3  35773  dfon2lem4  35774  dfon2lem6  35776  dfon2lem9  35779  dfon2  35780  hbimtg  35794  hbaltg  35795  dfrdg4  35939  btwntriv2  36000  btwncomim  36001  btwnswapid  36005  btwnexch3  36008  ifscgr  36032  lineunray  36135  hilbert1.2  36143  cldbnd  36314  tailfb  36365  meran3  36401  arg-ax  36404  ontopbas  36416  onsuct0  36429  limsucncmpi  36433  ordcmp  36435  onint1  36437  weiunpo  36453  bj-syl66ib  36543  bj-gl4  36583  bj-alexim  36615  bj-nfimt  36626  bj-ax6e  36656  bj-hbalt  36669  axc11n11r  36671  bj-nnfim  36734  bj-nnfan  36736  bj-nnfor  36738  bj-nnford  36739  bj-nnflemaa  36750  bj-nnflemae  36752  bj-19.21t  36757  bj-19.23t  36758  bj-19.42t  36761  bj-sbft  36763  bj-hbsb3t  36776  bj-cbv2hv  36785  bj-equsal1t  36810  bj-0int  37089  bj-bary1lem1  37299  topdifinffinlem  37335  isbasisrelowllem1  37343  isbasisrelowllem2  37344  iooelexlt  37350  finorwe  37370  finxpreclem1  37377  finxpreclem2  37378  isinf2  37393  fvineqsneu  37399  fvineqsneq  37400  pibt2  37405  wl-spae  37509  wl-19.8eqv  37511  wl-nfeqfb  37524  wl-mo3t  37564  wl-ax11-lem3  37575  fin2so  37601  poimirlem29  37643  poimirlem30  37644  poimirlem31  37645  poimirlem32  37646  ismblfin  37655  indexdom  37728  fzmul  37735  heibor1lem  37803  heibor  37815  exidu1  37850  rngoideu  37897  zerdivemp1x  37941  ispridl2  38032  cnf1dd  38084  cnf2dd  38085  cnfn1dd  38086  cnfn2dd  38087  orcomdd  38161  disjlem14  38790  disjdmqsss  38794  disjdmqscossss  38795  prtlem14  38867  prter2  38874  aev-o  38924  ax12eq  38934  ax12el  38935  ax12indn  38936  ax12indi  38937  lsatn0  38992  lsatcmp  38996  lsatcv0  39024  lfl1dim  39114  lfl1dim2N  39115  lkrss2N  39162  lub0N  39182  glb0N  39186  glbconxN  39372  hl2at  39399  cvrexchlem  39413  cvratlem  39415  cvrat4  39437  psubspi  39741  pointpsubN  39745  elpaddn0  39794  paddasslem17  39830  ispsubcl2N  39941  ldilval  40107  trlord  40563  diaelrnN  41039  cdlemm10N  41112  cdlemn11pre  41204  dihord2pre  41219  dihglblem2N  41288  dihglblem3N  41289  mapdrvallem2  41639  ioin9i8  42195  sn-sup2  42479  incssnn0  42699  fphpd  42804  rmxycomplete  42906  dford3lem1  43015  iocinico  43201  onsupnmax  43217  cantnfresb  43313  cantnf2  43314  tfsconcatb0  43333  tfsconcat0b  43335  sdomne0  43402  sdomne0d  43403  ensucne0OLD  43519  al3im  43636  brtrclfv2  43716  frege129d  43752  frege60a  43867  frege60c  43912  frege70  43922  rfovcnvf1od  43993  clsk1indlem3  44032  neik0pk1imk0  44036  gneispace  44123  gneispaceel2  44133  gneispacess2  44135  dvconstbi  44323  axc5c4c711toc7  44393  axc5c4c711to11  44394  pm14.24  44421  sbiota1  44423  bi33imp12  44481  bi123imp0  44486  ee233  44509  vk15.4j  44518  ssralv2  44521  alrim3con13v  44523  tratrb  44526  onfrALTlem3  44534  onfrALTlem2  44536  19.41rg  44540  hbimpg  44544  hbalg  44545  ax6e2ndeq  44549  e2  44621  ee223  44624  sspwtrALT  44811  sspwtrALT2  44812  suctrALT2  44826  trintALT  44870  isosctrlem1ALT  44923  relpmin  44942  traxext  44967  modelaxreplem2  44969  ssclaxsep  44972  fnchoice  45023  mptfnd  45236  stoweidlem62  46060  2reu8i  47114  2reuimp  47116  ffnafv  47172  lswn0  47445  reupr  47523  reuopreuprim  47527  requad2  47624  bgoldbnnsum3prm  47805  bgoldbtbndlem2  47807  bgoldbtbndlem4  47809  gricsym  47921  gpgedgvtx1  48053  ply1mulgsumlem2  48376  iunord  49665  setrec2fun  49681