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  870  pm2.37  985  pm2.81  986  oplem1  1071  3jao  1451  impsingle  1656  al2im  1843  exlimdv  1962  19.23v  1971  spimfw  1994  ax13b  2061  nf5-1  2179  hbald  2202  19.8a  2216  spimedv  2232  19.9d  2238  sbequ1  2283  sbft  2304  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  3676  2reu1  3850  reuss2  4278  reupick2  4283  elpwunsn  4649  pwpw0  4778  sssn  4791  iuneqconst  4967  disjiun  5096  trun  5228  reusv1  5367  reusv3i  5374  ralxfrALT  5385  exneq  5416  opth1  5456  copsexgwOLD  5472  copsexg  5473  opelopabt  5515  solin  5595  wefrc  5654  frinxp  5743  ssrelrn  5883  dmcosseq  5967  dmcosseqOLD  5968  reuop  6294  ordunidif  6411  oneqmini  6414  suctr  6449  ordsssuc2  6454  iotan0  6526  fv3  6899  ndmfv  6913  ssimaex  6966  fvopab3ig  6985  iinpreima  7064  fvcofneq  7088  dff3  7095  dff4  7096  ffnfv  7114  fnsnr  7161  fprb  7192  elunirn  7249  f1mpt  7259  isomin  7335  oprabidw  7443  oprabid  7444  mpoeq123  7484  sorpsscmpl  7733  dfwe2  7771  ssorduni  7776  ssonprc  7784  nlimsucg  7836  ordunisuc2  7838  tfinds  7854  ssnlim  7880  f1oweALT  7967  mptcnfimad  7981  el2mpocl  8079  f1o2ndf1  8115  frxp  8120  soxp  8123  poxp2  8137  poxp3  8144  poseq  8152  brtpos  8229  rntpos  8233  dftpos4  8239  onfununi  8326  onnseq  8329  smores2  8339  smo11  8349  tfr3  8384  rdglim2  8417  tz7.48lem  8426  tz7.49  8430  seqomlem2  8436  oawordex  8540  oa00  8542  oaass  8544  om00  8558  odi  8562  omass  8563  oeordi  8571  oelim2  8579  omsmo  8642  eroveu  8808  eceqoveq  8818  map0g  8880  fundmen  9026  sdomdif  9111  onsdominel  9112  pssnn  9151  nneneq  9188  php3  9191  f1finf1o  9231  findcard3  9241  unblem1  9250  fiint  9284  ixpfi2  9305  dffi2  9381  elfiun  9388  fisup2g  9427  fiinf2g  9460  wemaplem2  9507  elirrv  9557  elirrvOLD  9558  preleqALT  9584  inf3lem2  9596  inf3lem3  9597  inf3lem6  9600  noinfep  9627  epfrs  9698  tcmin  9706  r1sdom  9744  tz9.12lem3  9759  rankelb  9794  bndrank  9811  rankunb  9820  rankuni2b  9823  cplem1  9877  cplem1OLD  9878  kardenOLD  9887  carduni  9974  infxpenlem  10004  dfac8alem  10020  alephdom  10072  cardinfima  10088  alephval3  10101  dfac5lem4  10117  dfac5lem5  10118  dfac5  10119  dfac2b  10121  kmlem13  10153  nnadju  10188  ackbij1b  10228  cfub  10238  coflim  10251  cflim2  10253  cfslbn  10257  cfslb2n  10258  cofsmo  10259  cfsmolem  10260  sornom  10267  fincssdom  10313  isf32lem1  10343  isf32lem2  10344  isf32lem9  10351  isf34lem4  10367  isfin1-3  10376  axcc4  10429  domtriomlem  10432  axdc2lem  10438  axdc3lem2  10441  zorn2lem4  10489  zorn2lem6  10491  zornn0g  10495  uniimadom  10534  cardmin  10554  ficard  10555  konigthlem  10559  alephreg  10573  cfpwsdom  10575  axextnd  10582  fpwwe2lem5  10626  fpwwe2lem11  10632  fpwwe2lem12  10633  fpwwe2  10634  canthp1lem2  10644  gchpwdom  10661  winalim2  10687  tskuni  10774  grupr  10788  grur1a  10810  axgroth6  10819  grothomex  10820  eltskm  10834  addclpi  10883  nqereu  10920  ltexnq  10966  nsmallnq  10968  genpn0  10994  genpss  10995  genpnmax  10998  ltaddpr  11025  reclem3pr  11040  reclem4pr  11041  suplem1pr  11043  supsrlem  11102  1re  11214  dedekindle  11380  addrid  11396  negn0  11649  negf1o  11650  negfi  12170  sup2  12177  supadd  12189  supmullem1  12191  supmullem2  12192  zmulcl  12649  zeo  12688  uz11  12893  uzwo  12941  eqreznegel  12964  lbzbi  12966  qextlt  13235  qextle  13236  xrsupsslem  13339  xrinfmsslem  13340  supxrun  13348  supxrpnf  13350  supxrunb1  13351  supxrunb2  13352  fzm1  13642  uzrdgfni  14001  hasheqf1oi  14394  hashreshashfun  14483  leisorel  14504  fundmge2nop0  14546  wrdsymb0  14593  swrdnnn0nd  14701  swrdccatin2d  14788  cshinj  14855  repswcshw  14856  rennim  15297  01sqrexlem6  15305  caubnd  15417  sqreulem  15418  caucvgrlem  15731  fsumcvg  15770  supcvg  15917  prodeq2ii  15972  fprodcvg  15991  prodmo  15997  dvdslelem  16373  bitsinv1lem  16505  bitsshft  16539  smuval2  16546  smupvallem  16547  gcdcllem1  16563  bezoutlem2  16604  bezoutlem3  16605  algcvga  16643  isprm3  16747  isprm5  16772  oddprmdvds  16969  vdwlem13  17059  vdwnnlem1  17061  vdwnnlem3  17063  ramub1lem1  17092  prmgaplem5  17121  imasaddfnlem  17588  divsfval  17607  catpropd  17771  joindmss  18439  meetdmss  18453  psdmrn  18635  odlem1  19611  gexlem1  19655  cygctb  19968  rngisomring1  20557  lmodfopnelem1  21030  islss  21066  lspsneq0  21144  lspsneq  21257  psgnodpmr  21751  obselocv  21889  mvrf1  22146  evlseu  22245  mpfrcl  22247  ppttop  23175  epttop  23177  elcls  23241  restntr  23350  cnprest  23457  regsep  23502  nrmsep3  23523  lmmo  23548  cmpsublem  23567  cmpsub  23568  hauscmplem  23574  txcnpi  23776  txcnp  23788  fbun  24008  fbfinnfr  24009  trfbas2  24011  fgcl  24046  filssufilg  24079  ufinffr  24097  isfcls  24177  fclsrest  24192  flimfnfcls  24196  alexsubALTlem2  24216  alexsubALTlem3  24217  alexsubALTlem4  24218  alexsubALT  24219  cnextcn  24235  imasf1oxms  24657  metequiv2  24678  tngngpim  24827  iccpnfcnv  25114  iccpnfhmeo  25115  iscau2  25447  caun0  25451  minveclem3b  25598  itg1climres  25884  mbfi1fseqlem4  25888  ellimc3  26049  limccnp2  26062  dvlip  26163  itgsubstlem  26218  elply2  26364  coefv0  26416  coemulc  26423  ulmss  26571  sineq0  26700  scvxcvx  27161  sqf11  27314  ppiublem1  27377  fsumvma  27388  2sq2  27608  ostth  27814  ltsres  27837  nosepdmlem  27858  nobdaymin  27957  nocvxminlem  27958  addsprop  28180  mpteleeOLD  29256  brbtwn2  29266  colinearalg  29271  axcontlem4  29328  upgrres1  29674  usgr2trlncl  30120  umgrclwwlkge2  30353  upgr4cycl4dv4e  30547  1to3vfriendship  30643  3cyclfrgrrn1  30647  n4cyclfrgr  30653  frgrncvvdeqlem8  30668  frgrwopreg  30685  2clwwlk2clwwlk  30712  numclwwlk2lem1  30738  frgrreg  30756  frgrogt3nreg  30759  nmcvcn  31058  chlimi  31597  ocsh  31646  shsvs  31686  h1datomi  31944  stcl  32579  stge0  32587  stle1  32588  stm1addi  32608  stm1add3i  32610  cvnsym  32653  mdbr2  32659  dmdbr2  32666  mdsl0  32673  mdsl1i  32684  mdsl2i  32685  cvmdi  32687  atexch  32744  atcvat4i  32760  cdj1i  32796  1arithufdlem4  33846  xrge0iifcnv  34332  esumpr2  34466  sigaclci  34531  cntmeas  34625  mbfmcnt  34667  ballotlemfc0  34892  ballotlemfcc  34893  bnj1379  35227  bnj607  35313  bnj908  35328  bnj938  35334  bnj1174  35400  bnj1280  35417  f1resrcmplf1dlem  35483  fnrelpredd  35491  r1filimi  35506  fineqvinfep  35546  tz9.1regs  35555  axsepg2  35561  axsepg4  35564  axnulg  35566  axpowg2  35568  axpowg3  35569  kardcard2b  35586  ackardcard  35588  cusgr3cyclex  35636  loop1cycl  35637  acycgrislfgr  35652  pthacycspth  35657  iccllysconn  35750  satffunlem1lem1  35902  satfvel  35912  sate0fv0  35917  antnestlaw2  36192  funpsstri  36266  fundmpss  36267  dfon2lem3  36283  dfon2lem4  36284  dfon2lem6  36286  dfon2lem9  36289  dfon2  36290  hbimtg  36304  hbaltg  36305  dfrdg4  36451  btwntriv2  36512  btwncomim  36513  btwnswapid  36517  btwnexch3  36520  ifscgr  36544  lineunray  36647  hilbert1.2  36655  cldbnd  36865  tailfb  36916  meran3  36952  arg-ax  36955  ontopbas  36967  onsuct0  36980  limsucncmpi  36984  ordcmp  36986  onint1  36988  weiunpo  37004  axtcond  37017  axuntco  37018  dfttc4lem2  37068  bj-bisimpl  37173  bj-bisimpr  37174  bj-syl66ib  37175  bj-gl4  37216  bj-alexim  37261  bj-nfimt  37273  bj-spvw  37285  bj-cbvalvv  37289  bj-ax6e  37318  bj-hbald  37332  axc11n11r  37336  bj-nnfim  37405  bj-nnfan  37407  bj-nnfor  37409  bj-nnford  37410  bj-19.21t  37414  bj-19.23t  37415  bj-19.42t  37418  bj-sbft  37431  bj-nnflemaa  37439  bj-nnflemae  37441  bj-hbsb3t  37451  bj-cbv2hv  37460  bj-equsal1t  37485  bj-axreprepsep  37740  bj-0int  37771  bj-bary1lem1  37983  topdifinffinlem  38021  isbasisrelowllem1  38029  isbasisrelowllem2  38030  iooelexlt  38036  finorwe  38056  finxpreclem1  38063  finxpreclem2  38064  isinf2  38079  fvineqsneu  38085  fvineqsneq  38086  pibt2  38091  wl-spae  38204  wl-19.8eqv  38206  wl-nfeqfb  38219  wl-mo3t  38259  wl-eujustlem1  38271  fin2so  38286  poimirlem29  38328  poimirlem30  38329  poimirlem31  38330  poimirlem32  38331  ismblfin  38340  indexdom  38413  fzmul  38420  heibor1lem  38488  heibor  38500  exidu1  38535  rngoideu  38582  zerdivemp1x  38626  ispridl2  38717  cnf1dd  38767  cnf2dd  38768  cnfn1dd  38769  cnfn2dd  38770  orcomdd  38844  disjlem14  39578  disjdmqsss  39582  disjdmqscossss  39583  prtlem14  39676  prter2  39683  aev-o  39733  ax12eq  39743  ax12el  39744  ax12indn  39745  ax12indi  39746  lsatn0  39801  lsatcmp  39805  lsatcv0  39833  lfl1dim  39923  lfl1dim2N  39924  lkrss2N  39971  lub0N  39991  glb0N  39995  glbconxN  40180  hl2at  40207  cvrexchlem  40221  cvratlem  40223  cvrat4  40245  psubspi  40549  pointpsubN  40553  elpaddn0  40602  paddasslem17  40638  ispsubcl2N  40749  ldilval  40915  trlord  41371  diaelrnN  41847  cdlemm10N  41920  cdlemn11pre  42012  dihord2pre  42027  dihglblem2N  42096  dihglblem3N  42097  mapdrvallem2  42447  ioin9i8  43004  sn-sup2  43293  incssnn0  43470  fphpd  43571  rmxycomplete  43672  dford3lem1  43781  iocinico  43967  onsupnmax  43983  cantnfresb  44079  cantnf2  44080  tfsconcatb0  44099  tfsconcat0b  44101  sdomne0  44167  sdomne0d  44168  ensucne0OLD  44284  al3im  44401  brtrclfv2  44481  frege129d  44517  frege60a  44632  frege60c  44677  frege70  44687  rfovcnvf1od  44758  clsk1indlem3  44797  neik0pk1imk0  44801  gneispace  44888  gneispaceel2  44898  gneispacess2  44900  dvconstbi  45072  axc5c4c711toc7  45142  axc5c4c711to11  45143  pm14.24  45170  sbiota1  45172  bi33imp12  45228  bi123imp0  45233  ee233  45256  vk15.4j  45265  ssralv2  45268  alrim3con13v  45270  tratrb  45273  onfrALTlem3  45281  onfrALTlem2  45283  19.41rg  45287  hbimpg  45291  hbalg  45292  ax6e2ndeq  45296  e2  45368  ee223  45371  sspwtrALT  45558  sspwtrALT2  45559  suctrALT2  45573  trintALT  45617  isosctrlem1ALT  45670  relpmin  45689  traxext  45714  modelaxreplem2  45716  ssclaxsep  45719  fnchoice  45777  mptfnd  45985  stoweidlem62  46804  2reu8i  47878  2reuimp  47880  ffnafv  47936  lswn0  48221  reupr  48299  reuopreuprim  48303  requad2  48416  bgoldbnnsum3prm  48597  bgoldbtbndlem2  48599  bgoldbtbndlem4  48601  gricsym  48714  gpgedgvtx1  48855  ply1mulgsumlem2  49195  iunord  50482  setrec2fun  50498