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  2217  spimedv  2233  19.9d  2239  sbequ1  2283  sbft  2303  cbv2w  2366  spimed  2417  cbv2  2432  cbv2h  2435  ax12  2452  axc11n  2455  equvini  2484  sb2  2508  sb4a  2509  mo3  2589  mopick  2650  moexexlem  2651  dvelimdc  2946  necon1ad  2972  necon4bd  2975  rsp2  3279  mo2icl  3671  2reu1  3844  reuss2  4271  reupick2  4276  elpwunsn  4644  pwpw0  4773  sssn  4786  iuneqconst  4962  disjiun  5090  trun  5222  reusv1  5358  reusv3i  5365  ralxfrALT  5376  exneq  5403  opth1  5443  copsexgwOLD  5459  copsexg  5460  opelopabt  5502  solin  5582  wefrc  5641  frinxp  5730  ssrelrn  5872  dmcosseq  5956  dmcosseqOLD  5957  reuop  6285  ordunidif  6402  oneqmini  6405  suctr  6440  ordsssuc2  6445  iotan0  6517  fv3  6891  ndmfv  6905  ssimaex  6958  fvopab3ig  6977  iinpreima  7057  fvcofneq  7081  dff3  7088  dff4  7089  ffnfv  7107  fnsnr  7156  fprb  7187  elunirn  7243  f1mpt  7253  f1resrcmplf1dlem  7266  isomin  7333  oprabidw  7439  oprabid  7440  mpoeq123  7480  sorpsscmpl  7733  dfwe2  7771  ssorduni  7776  ssonprc  7784  nlimsucg  7836  ordunisuc2  7838  tfinds  7854  ssnlim  7880  f1oweALT  7967  mptcnfimad  7981  el2mpocl  8080  f1o2ndf1  8116  frxp  8121  soxp  8124  poxp2  8138  poxp3  8145  poseq  8153  brtpos  8230  rntpos  8234  dftpos4  8240  onfununi  8327  onnseq  8330  smores2  8340  smo11  8350  tfr3  8385  rdglim2  8418  tz7.48lemOLD  8429  tz7.49  8433  seqomlem2  8439  oawordex  8543  oa00  8545  oaass  8547  om00  8561  odi  8565  omass  8566  oeordi  8574  oelim2  8582  omsmo  8645  eroveu  8811  eceqoveq  8821  map0g  8890  fundmen  9037  sdomdif  9122  onsdominel  9123  pssnn  9162  nneneq  9199  php3  9202  f1finf1o  9242  findcard3  9252  unblem1  9262  fiint  9296  ixpfi2  9317  dffi2  9393  elfiun  9400  fisup2g  9439  fiinf2g  9472  wemaplem2  9519  elirrv  9569  elirrvOLD  9570  preleqALT  9596  inf3lem2  9608  inf3lem3  9609  inf3lem6  9612  noinfep  9639  epfrs  9710  tcmin  9718  r1sdom  9756  tz9.12lem3  9771  rankelb  9806  bndrank  9827  rankunb  9837  rankuni2b  9840  r1filimi  9876  cplem1  9922  cplem1OLD  9923  kardenOLD  9932  setrec2fun  9945  carduni  10034  infxpenlem  10064  dfac8alem  10080  alephdom  10132  cardinfima  10148  alephval3  10161  dfac5lem4  10177  dfac5lem5  10178  dfac5  10179  dfac2b  10181  kmlem13  10213  nnadju  10248  ackbij1b  10288  cfub  10298  coflim  10311  cflim2  10313  cfslbn  10317  cfslb2n  10318  cofsmo  10319  cfsmolem  10320  sornom  10327  fincssdom  10373  isf32lem1  10403  isf32lem2  10404  isf32lem9  10411  isf34lem4  10427  isfin1-3  10436  axcc4  10489  domtriomlem  10492  axdc2lem  10498  axdc3lem2  10501  zorn2lem4  10549  zorn2lem6  10551  zornn0g  10555  uniimadom  10600  cardmin  10620  ficard  10621  konigthlem  10625  alephreg  10639  cfpwsdom  10641  axextnd  10648  fpwwe2lem5  10692  fpwwe2lem11  10698  fpwwe2lem12  10699  fpwwe2  10700  canthp1lem2  10710  gchpwdom  10727  winalim2  10753  tskuni  10840  grupr  10854  grur1a  10876  axgroth6  10885  grothomex  10886  eltskm  10900  addclpi  10949  nqereu  10986  ltexnq  11032  nsmallnq  11034  genpn0  11060  genpss  11061  genpnmax  11064  ltaddpr  11091  reclem3pr  11106  reclem4pr  11107  suplem1pr  11109  supsrlem  11168  1re  11280  dedekindle  11446  addrid  11462  negn0  11715  negf1o  11716  negfi  12236  sup2  12243  supadd  12255  supmullem1  12257  supmullem2  12258  zmulcl  12715  zeo  12755  uz11  12960  uzwo  13008  eqreznegel  13031  lbzbi  13033  qextlt  13303  qextle  13304  xrsupsslem  13407  xrinfmsslem  13408  supxrun  13416  supxrpnf  13418  supxrunb1  13419  supxrunb2  13420  fzm1  13710  uzrdgfni  14070  hasheqf1oi  14463  hashreshashfun  14552  leisorel  14573  fundmge2nop0  14615  wrdsymb0  14662  swrdnnn0nd  14774  swrdccatin2d  14861  cshinj  14930  repswcshw  14931  rennim  15374  01sqrexlem6  15382  caubnd  15494  sqreulem  15495  caucvgrlem  15808  fsumcvg  15846  supcvg  15993  prodeq2ii  16048  fprodcvg  16065  prodmo  16071  dvdslelem  16447  bitsinv1lem  16579  bitsshft  16613  smuval2  16620  smupvallem  16621  gcdcllem1  16637  bezoutlem2  16678  bezoutlem3  16679  algcvga  16717  isprm3  16821  isprm5  16846  oddprmdvds  17043  vdwlem13  17133  vdwnnlem1  17135  vdwnnlem3  17137  ramub1lem1  17166  prmgaplem5  17195  imasaddfnlem  17662  divsfval  17681  catpropd  17845  joindmss  18513  meetdmss  18527  psdmrn  18709  odlem1  19711  gexlem1  19755  cygctb  20068  rngisomring1  20660  lmodfopnelem1  21135  islss  21171  lspsneq0  21249  lspsneq  21362  psgnodpmr  21858  obselocv  21996  mvrf1  22255  evlseu  22354  mpfrcl  22356  ppttop  23287  epttop  23289  elcls  23353  restntr  23462  cnprest  23569  regsep  23614  nrmsep3  23635  lmmo  23660  cmpsublem  23679  cmpsub  23680  hauscmplem  23686  txcnpi  23889  txcnp  23901  fbun  24121  fbfinnfr  24122  trfbas2  24124  fgcl  24159  filssufilg  24192  ufinffr  24210  isfcls  24290  fclsrest  24305  flimfnfcls  24309  alexsubALTlem2  24329  alexsubALTlem3  24330  alexsubALTlem4  24331  alexsubALT  24332  cnextcn  24348  imasf1oxms  24770  metequiv2  24791  tngngpim  24940  iccpnfcnv  25227  iccpnfhmeo  25228  iscau2  25560  caun0  25564  minveclem3b  25711  itg1climres  25997  mbfi1fseqlem4  26001  ellimc3  26161  limccnp2  26174  dvlip  26275  itgsubstlem  26330  elply2  26476  coefv0  26529  coemulc  26536  ulmss  26688  sineq0  26816  scvxcvx  27277  sqf11  27430  ppiublem1  27493  fsumvma  27504  2sq2  27724  ostth  27930  ltsres  27953  nosepdmlem  27974  nobdaymin  28073  nocvxminlem  28074  addsprop  28296  mpteleeOLD  29407  brbtwn2  29417  colinearalg  29422  axcontlem4  29479  upgrres1  29828  usgr2trlncl  30280  umgrclwwlkge2  30516  loop1cycl  30678  upgr4cycl4dv4e  30720  1to3vfriendship  30816  3cyclfrgrrn1  30820  n4cyclfrgr  30826  frgrncvvdeqlem8  30841  frgrwopreg  30858  2clwwlk2clwwlk  30885  numclwwlk2lem1  30911  frgrreg  30929  frgrogt3nreg  30932  nmcvcn  31231  chlimi  31770  ocsh  31819  shsvs  31859  h1datomi  32117  stcl  32752  stge0  32760  stle1  32761  stm1addi  32781  stm1add3i  32783  cvnsym  32826  mdbr2  32832  dmdbr2  32839  mdsl0  32846  mdsl1i  32857  mdsl2i  32858  cvmdi  32860  atexch  32917  atcvat4i  32933  cdj1i  32969  1arithufdlem4  34013  xrge0iifcnv  34499  esumpr2  34633  sigaclci  34698  cntmeas  34793  mbfmcnt  34835  ballotlemfc0  35060  ballotlemfcc  35061  bnj1379  35395  bnj607  35481  bnj908  35496  bnj938  35502  bnj1174  35568  bnj1280  35585  fnrelpredd  35651  fineqvinfep  35718  tz9.1regs  35727  axsepg2  35733  axsepg4  35736  axnulg  35738  axpowg2  35740  axpowg3  35741  kardcard2b  35758  ackardcard  35760  cusgr3cyclex  35832  acycgrislfgr  35838  pthacycspth  35843  iccllysconn  35936  satffunlem1lem1  36088  satfvel  36098  sate0fv0  36103  antnestlaw2  36378  funpsstri  36452  fundmpss  36453  dfon2lem3  36469  dfon2lem4  36470  dfon2lem6  36472  dfon2lem9  36475  dfon2  36476  hbimtg  36490  hbaltg  36491  dfrdg4  36637  btwntriv2  36699  btwncomim  36700  btwnswapid  36704  btwnexch3  36707  ifscgr  36731  lineunray  36834  hilbert1.2  36842  cldbnd  37036  tailfb  37087  meran3  37123  arg-ax  37126  ontopbas  37138  onsuct0  37151  limsucncmpi  37155  ordcmp  37157  onint1  37159  weiunpo  37175  axtcond  37188  axuntco  37189  dfttc4lem2  37239  bj-bisimpl  37344  bj-bisimpr  37345  bj-syl66ib  37346  bj-gl4  37387  bj-alexim  37432  bj-nfimt  37444  bj-spvw  37456  bj-cbvalvv  37460  bj-ax6e  37489  bj-hbald  37503  axc11n11r  37507  bj-nnfim  37576  bj-nnfan  37578  bj-nnfor  37580  bj-nnford  37581  bj-19.21t  37585  bj-19.23t  37586  bj-19.42t  37589  bj-sbft  37602  bj-nnflemaa  37610  bj-nnflemae  37612  bj-hbsb3t  37622  bj-cbv2hv  37631  bj-equsal1t  37656  bj-axreprepsep  37911  bj-0int  37942  bj-bary1lem1  38152  topdifinffinlem  38190  isbasisrelowllem1  38198  isbasisrelowllem2  38199  iooelexlt  38205  finorwe  38225  finxpreclem1  38232  finxpreclem2  38233  isinf2  38248  fvineqsneu  38254  fvineqsneq  38255  pibt2  38260  wl-spae  38373  wl-19.8eqv  38375  wl-nfeqfb  38388  wl-mo3t  38428  wl-eujustlem1  38440  fin2so  38450  poimirlem29  38487  poimirlem30  38488  poimirlem31  38489  poimirlem32  38490  ismblfin  38499  indexdom  38588  fzmul  38595  heibor1lem  38663  heibor  38675  exidu1  38710  rngoideu  38757  zerdivemp1x  38801  ispridl2  38892  cnf1dd  38942  cnf2dd  38943  cnfn1dd  38944  cnfn2dd  38945  orcomdd  39019  disjlem14  39753  disjdmqsss  39757  disjdmqscossss  39758  prtlem14  39851  prter2  39858  aev-o  39908  ax12eq  39918  ax12el  39919  ax12indn  39920  ax12indi  39921  lsatn0  39976  lsatcmp  39980  lsatcv0  40008  lfl1dim  40098  lfl1dim2N  40099  lkrss2N  40146  lub0N  40166  glb0N  40170  glbconxN  40355  hl2at  40382  cvrexchlem  40396  cvratlem  40398  cvrat4  40420  psubspi  40724  pointpsubN  40728  elpaddn0  40777  paddasslem17  40813  ispsubcl2N  40924  ldilval  41090  trlord  41546  diaelrnN  42022  cdlemm10N  42095  cdlemn11pre  42187  dihord2pre  42202  dihglblem2N  42271  dihglblem3N  42272  mapdrvallem2  42622  ioin9i8  43179  sn-sup2  43483  incssnn0  43660  fphpd  43761  rmxycomplete  43862  dford3lem1  43971  iocinico  44157  onsupnmax  44173  cantnfresb  44269  cantnf2  44270  tfsconcatb0  44289  tfsconcat0b  44291  sdomne0  44357  sdomne0d  44358  ensucne0OLD  44474  al3im  44591  brtrclfv2  44671  frege129d  44707  frege60a  44822  frege60c  44867  frege70  44877  rfovcnvf1od  44948  clsk1indlem3  44987  neik0pk1imk0  44991  gneispace  45078  gneispaceel2  45088  gneispacess2  45090  dvconstbi  45262  axc5c4c711toc7  45332  axc5c4c711to11  45333  pm14.24  45360  sbiota1  45362  bi33imp12  45418  bi123imp0  45423  ee233  45446  vk15.4j  45455  ssralv2  45458  alrim3con13v  45460  tratrb  45463  onfrALTlem3  45471  onfrALTlem2  45473  19.41rg  45477  hbimpg  45481  hbalg  45482  ax6e2ndeq  45486  e2  45558  ee223  45561  sspwtrALT  45748  sspwtrALT2  45749  suctrALT2  45763  trintALT  45807  isosctrlem1ALT  45860  relpmin  45879  traxext  45904  modelaxreplem2  45906  ssclaxsep  45909  fnchoice  45967  mptfnd  46175  stoweidlem62  46994  2reu8i  48105  2reuimp  48107  ffnafv  48163  lswn0  48448  reupr  48526  reuopreuprim  48530  requad2  48643  bgoldbnnsum3prm  48824  bgoldbtbndlem2  48826  bgoldbtbndlem4  48828  gricsym  48941  gpgedgvtx1  49082  ply1mulgsumlem2  49421  iunord  50706