Theorem syl6 36

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 31	1 ⊢ (𝜑 → (𝜓 → 𝜃))

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  syl56  37  syl6com  38  a1dd  51  syl6mpi  68  syl6c  71  syl10  80  com34  92  con1d  146  expi  166  looinv  206  imbitrdi  254  imbitrrdi  255  biimtrdi  256  biimtrrdi  257  jaoi  871  pm2.37  986  pm2.81  987  oplem1  1072  3jao  1452  impsingle  1660  al2im  1847  exlimdv  1966  19.23v  1975  spimfw  1998  ax13b  2065  nf5-1  2182  hbald  2205  19.8a  2219  spimedv  2235  19.9d  2241  sbequ1  2285  sbft  2305  cbv2w  2368  spimed  2419  cbv2  2434  cbv2h  2437  ax12  2454  axc11n  2457  equvini  2486  sb2  2510  sb4a  2511  mo3  2591  mopick  2652  moexexlem  2653  dvelimdc  2948  necon1ad  2974  necon4bd  2977  rsp2  3281  mo2icl  3675  2reu1  3848  reuss2  4275  reupick2  4280  elpwunsn  4648  pwpw0  4777  sssn  4790  iuneqconst  4966  disjiun  5095  trun  5227  reusv1  5366  reusv3i  5373  ralxfrALT  5384  exneq  5415  opth1  5455  copsexgwOLD  5471  copsexg  5472  opelopabt  5514  solin  5594  wefrc  5653  frinxp  5742  ssrelrn  5882  dmcosseq  5966  dmcosseqOLD  5967  reuop  6295  ordunidif  6412  oneqmini  6415  suctr  6450  ordsssuc2  6455  iotan0  6527  fv3  6900  ndmfv  6914  ssimaex  6967  fvopab3ig  6986  iinpreima  7065  fvcofneq  7089  dff3  7096  dff4  7097  ffnfv  7115  fnsnr  7164  fprb  7195  elunirn  7251  f1mpt  7261  f1resrcmplf1dlem  7274  isomin  7341  oprabidw  7447  oprabid  7448  mpoeq123  7488  sorpsscmpl  7738  dfwe2  7776  ssorduni  7781  ssonprc  7789  nlimsucg  7841  ordunisuc2  7843  tfinds  7859  ssnlim  7885  f1oweALT  7972  mptcnfimad  7986  el2mpocl  8086  f1o2ndf1  8122  frxp  8127  soxp  8130  poxp2  8144  poxp3  8151  poseq  8159  brtpos  8236  rntpos  8240  dftpos4  8246  onfununi  8333  onnseq  8336  smores2  8346  smo11  8356  tfr3  8391  rdglim2  8424  tz7.48lem  8433  tz7.49  8437  seqomlem2  8443  oawordex  8547  oa00  8549  oaass  8551  om00  8565  odi  8569  omass  8570  oeordi  8578  oelim2  8586  omsmo  8649  eroveu  8815  eceqoveq  8825  map0g  8894  fundmen  9041  sdomdif  9126  onsdominel  9127  pssnn  9166  nneneq  9203  php3  9206  f1finf1o  9246  findcard3  9256  unblem1  9265  fiint  9299  ixpfi2  9320  dffi2  9396  elfiun  9403  fisup2g  9442  fiinf2g  9475  wemaplem2  9522  elirrv  9572  elirrvOLD  9573  preleqALT  9599  inf3lem2  9611  inf3lem3  9612  inf3lem6  9615  noinfep  9642  epfrs  9713  tcmin  9721  r1sdom  9759  tz9.12lem3  9774  rankelb  9809  bndrank  9826  rankunb  9835  rankuni2b  9838  cplem1  9892  cplem1OLD  9893  kardenOLD  9902  carduni  9989  infxpenlem  10019  dfac8alem  10035  alephdom  10087  cardinfima  10103  alephval3  10116  dfac5lem4  10132  dfac5lem5  10133  dfac5  10134  dfac2b  10136  kmlem13  10168  nnadju  10203  ackbij1b  10243  cfub  10253  coflim  10266  cflim2  10268  cfslbn  10272  cfslb2n  10273  cofsmo  10274  cfsmolem  10275  sornom  10282  fincssdom  10328  isf32lem1  10358  isf32lem2  10359  isf32lem9  10366  isf34lem4  10382  isfin1-3  10391  axcc4  10444  domtriomlem  10447  axdc2lem  10453  axdc3lem2  10456  zorn2lem4  10504  zorn2lem6  10506  zornn0g  10510  uniimadom  10555  cardmin  10575  ficard  10576  konigthlem  10580  alephreg  10594  cfpwsdom  10596  axextnd  10603  fpwwe2lem5  10647  fpwwe2lem11  10653  fpwwe2lem12  10654  fpwwe2  10655  canthp1lem2  10665  gchpwdom  10682  winalim2  10708  tskuni  10795  grupr  10809  grur1a  10831  axgroth6  10840  grothomex  10841  eltskm  10855  addclpi  10904  nqereu  10941  ltexnq  10987  nsmallnq  10989  genpn0  11015  genpss  11016  genpnmax  11019  ltaddpr  11046  reclem3pr  11061  reclem4pr  11062  suplem1pr  11064  supsrlem  11123  1re  11235  dedekindle  11401  addrid  11417  negn0  11670  negf1o  11671  negfi  12191  sup2  12198  supadd  12210  supmullem1  12212  supmullem2  12213  zmulcl  12670  zeo  12710  uz11  12915  uzwo  12963  eqreznegel  12986  lbzbi  12988  qextlt  13257  qextle  13258  xrsupsslem  13361  xrinfmsslem  13362  supxrun  13370  supxrpnf  13372  supxrunb1  13373  supxrunb2  13374  fzm1  13664  uzrdgfni  14024  hasheqf1oi  14417  hashreshashfun  14506  leisorel  14527  fundmge2nop0  14569  wrdsymb0  14616  swrdnnn0nd  14728  swrdccatin2d  14815  cshinj  14884  repswcshw  14885  rennim  15328  01sqrexlem6  15336  caubnd  15448  sqreulem  15449  caucvgrlem  15762  fsumcvg  15800  supcvg  15947  prodeq2ii  16002  fprodcvg  16021  prodmo  16027  dvdslelem  16403  bitsinv1lem  16535  bitsshft  16569  smuval2  16576  smupvallem  16577  gcdcllem1  16593  bezoutlem2  16634  bezoutlem3  16635  algcvga  16673  isprm3  16777  isprm5  16802  oddprmdvds  16999  vdwlem13  17089  vdwnnlem1  17091  vdwnnlem3  17093  ramub1lem1  17122  prmgaplem5  17151  imasaddfnlem  17618  divsfval  17637  catpropd  17801  joindmss  18469  meetdmss  18483  psdmrn  18665  odlem1  19666  gexlem1  19710  cygctb  20023  rngisomring1  20613  lmodfopnelem1  21086  islss  21122  lspsneq0  21200  lspsneq  21313  psgnodpmr  21807  obselocv  21945  mvrf1  22204  evlseu  22303  mpfrcl  22305  ppttop  23236  epttop  23238  elcls  23302  restntr  23411  cnprest  23518  regsep  23563  nrmsep3  23584  lmmo  23609  cmpsublem  23628  cmpsub  23629  hauscmplem  23635  txcnpi  23838  txcnp  23850  fbun  24070  fbfinnfr  24071  trfbas2  24073  fgcl  24108  filssufilg  24141  ufinffr  24159  isfcls  24239  fclsrest  24254  flimfnfcls  24258  alexsubALTlem2  24278  alexsubALTlem3  24279  alexsubALTlem4  24280  alexsubALT  24281  cnextcn  24297  imasf1oxms  24719  metequiv2  24740  tngngpim  24889  iccpnfcnv  25176  iccpnfhmeo  25177  iscau2  25509  caun0  25513  minveclem3b  25660  itg1climres  25946  mbfi1fseqlem4  25950  ellimc3  26111  limccnp2  26124  dvlip  26225  itgsubstlem  26280  elply2  26426  coefv0  26478  coemulc  26485  ulmss  26633  sineq0  26762  scvxcvx  27223  sqf11  27376  ppiublem1  27439  fsumvma  27450  2sq2  27670  ostth  27876  ltsres  27899  nosepdmlem  27920  nobdaymin  28019  nocvxminlem  28020  addsprop  28242  mpteleeOLD  29353  brbtwn2  29363  colinearalg  29368  axcontlem4  29425  upgrres1  29774  usgr2trlncl  30226  umgrclwwlkge2  30462  loop1cycl  30624  upgr4cycl4dv4e  30666  1to3vfriendship  30762  3cyclfrgrrn1  30766  n4cyclfrgr  30772  frgrncvvdeqlem8  30787  frgrwopreg  30804  2clwwlk2clwwlk  30831  numclwwlk2lem1  30857  frgrreg  30875  frgrogt3nreg  30878  nmcvcn  31177  chlimi  31716  ocsh  31765  shsvs  31805  h1datomi  32063  stcl  32698  stge0  32706  stle1  32707  stm1addi  32727  stm1add3i  32729  cvnsym  32772  mdbr2  32778  dmdbr2  32785  mdsl0  32792  mdsl1i  32803  mdsl2i  32804  cvmdi  32806  atexch  32863  atcvat4i  32879  cdj1i  32915  1arithufdlem4  33959  xrge0iifcnv  34445  esumpr2  34579  sigaclci  34644  cntmeas  34739  mbfmcnt  34781  ballotlemfc0  35006  ballotlemfcc  35007  bnj1379  35341  bnj607  35427  bnj908  35442  bnj938  35448  bnj1174  35514  bnj1280  35531  fnrelpredd  35598  r1filimi  35613  fineqvinfep  35653  tz9.1regs  35662  axsepg2  35668  axsepg4  35671  axnulg  35673  axpowg2  35675  axpowg3  35676  kardcard2b  35693  ackardcard  35695  cusgr3cyclex  35727  acycgrislfgr  35733  pthacycspth  35738  iccllysconn  35831  satffunlem1lem1  35983  satfvel  35993  sate0fv0  35998  antnestlaw2  36273  funpsstri  36347  fundmpss  36348  dfon2lem3  36364  dfon2lem4  36365  dfon2lem6  36367  dfon2lem9  36370  dfon2  36371  hbimtg  36385  hbaltg  36386  dfrdg4  36532  btwntriv2  36594  btwncomim  36595  btwnswapid  36599  btwnexch3  36602  ifscgr  36626  lineunray  36729  hilbert1.2  36737  cldbnd  36947  tailfb  36998  meran3  37034  arg-ax  37037  ontopbas  37049  onsuct0  37062  limsucncmpi  37066  ordcmp  37068  onint1  37070  weiunpo  37086  axtcond  37099  axuntco  37100  dfttc4lem2  37150  bj-bisimpl  37255  bj-bisimpr  37256  bj-syl66ib  37257  bj-gl4  37298  bj-alexim  37343  bj-nfimt  37355  bj-spvw  37367  bj-cbvalvv  37371  bj-ax6e  37400  bj-hbald  37414  axc11n11r  37418  bj-nnfim  37487  bj-nnfan  37489  bj-nnfor  37491  bj-nnford  37492  bj-19.21t  37496  bj-19.23t  37497  bj-19.42t  37500  bj-sbft  37513  bj-nnflemaa  37521  bj-nnflemae  37523  bj-hbsb3t  37533  bj-cbv2hv  37542  bj-equsal1t  37567  bj-axreprepsep  37822  bj-0int  37853  bj-bary1lem1  38065  topdifinffinlem  38103  isbasisrelowllem1  38111  isbasisrelowllem2  38112  iooelexlt  38118  finorwe  38138  finxpreclem1  38145  finxpreclem2  38146  isinf2  38161  fvineqsneu  38167  fvineqsneq  38168  pibt2  38173  wl-spae  38286  wl-19.8eqv  38288  wl-nfeqfb  38301  wl-mo3t  38341  wl-eujustlem1  38353  fin2so  38363  poimirlem29  38400  poimirlem30  38401  poimirlem31  38402  poimirlem32  38403  ismblfin  38412  indexdom  38486  fzmul  38493  heibor1lem  38561  heibor  38573  exidu1  38608  rngoideu  38655  zerdivemp1x  38699  ispridl2  38790  cnf1dd  38840  cnf2dd  38841  cnfn1dd  38842  cnfn2dd  38843  orcomdd  38917  disjlem14  39651  disjdmqsss  39655  disjdmqscossss  39656  prtlem14  39749  prter2  39756  aev-o  39806  ax12eq  39816  ax12el  39817  ax12indn  39818  ax12indi  39819  lsatn0  39874  lsatcmp  39878  lsatcv0  39906  lfl1dim  39996  lfl1dim2N  39997  lkrss2N  40044  lub0N  40064  glb0N  40068  glbconxN  40253  hl2at  40280  cvrexchlem  40294  cvratlem  40296  cvrat4  40318  psubspi  40622  pointpsubN  40626  elpaddn0  40675  paddasslem17  40711  ispsubcl2N  40822  ldilval  40988  trlord  41444  diaelrnN  41920  cdlemm10N  41993  cdlemn11pre  42085  dihord2pre  42100  dihglblem2N  42169  dihglblem3N  42170  mapdrvallem2  42520  ioin9i8  43077  sn-sup2  43381  incssnn0  43558  fphpd  43659  rmxycomplete  43760  dford3lem1  43869  iocinico  44055  onsupnmax  44071  cantnfresb  44167  cantnf2  44168  tfsconcatb0  44187  tfsconcat0b  44189  sdomne0  44255  sdomne0d  44256  ensucne0OLD  44372  al3im  44489  brtrclfv2  44569  frege129d  44605  frege60a  44720  frege60c  44765  frege70  44775  rfovcnvf1od  44846  clsk1indlem3  44885  neik0pk1imk0  44889  gneispace  44976  gneispaceel2  44986  gneispacess2  44988  dvconstbi  45160  axc5c4c711toc7  45230  axc5c4c711to11  45231  pm14.24  45258  sbiota1  45260  bi33imp12  45316  bi123imp0  45321  ee233  45344  vk15.4j  45353  ssralv2  45356  alrim3con13v  45358  tratrb  45361  onfrALTlem3  45369  onfrALTlem2  45371  19.41rg  45375  hbimpg  45379  hbalg  45380  ax6e2ndeq  45384  e2  45456  ee223  45459  sspwtrALT  45646  sspwtrALT2  45647  suctrALT2  45661  trintALT  45705  isosctrlem1ALT  45758  relpmin  45777  traxext  45802  modelaxreplem2  45804  ssclaxsep  45807  fnchoice  45865  mptfnd  46073  stoweidlem62  46892  2reu8i  48003  2reuimp  48005  ffnafv  48061  lswn0  48346  reupr  48424  reuopreuprim  48428  requad2  48541  bgoldbnnsum3prm  48722  bgoldbtbndlem2  48724  bgoldbtbndlem4  48726  gricsym  48839  gpgedgvtx1  48980  ply1mulgsumlem2  49319  iunord  50604  setrec2fun  50620