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  204  imbitrdi  252  imbitrrdi  253  biimtrdi  254  biimtrrdi  255  jaoi  863  pm2.37  978  pm2.81  979  oplem1  1062  3jao  1433  impsingle  1634  al2im  1821  exlimdv  1940  19.23v  1949  spimfw  1972  ax13b  2039  nf5-1  2156  hbald  2179  19.8a  2193  spimedv  2209  19.9d  2215  sbequ1  2260  sbft  2281  cbv2w  2345  spimed  2396  cbv2  2411  cbv2h  2414  ax12  2431  axc11n  2434  equvini  2463  sb2  2487  sb4a  2488  mo3  2568  mopick  2629  moexexlem  2630  dvelimdc  2926  necon1ad  2952  necon4bd  2955  rsp2  3257  mo2icl  3662  2reu1  3836  reuss2  4261  reupick2  4266  elpwunsn  4623  pwpw0  4751  sssn  4764  iuneqconst  4940  disjiun  5067  trun  5197  reusv1  5333  reusv3i  5340  ralxfrALT  5351  exneq  5382  opth1  5422  copsexgwOLD  5438  copsexg  5439  opelopabt  5481  solin  5560  wefrc  5619  frinxp  5708  ssrelrn  5843  dmcosseq  5927  dmcosseqOLD  5928  reuop  6251  ordunidif  6367  oneqmini  6370  suctr  6405  ordsssuc2  6410  iotan0  6482  fv3  6852  ndmfv  6866  ssimaex  6919  fvopab3ig  6938  iinpreima  7017  fvcofneq  7041  dff3  7048  dff4  7049  ffnfv  7067  fnsnr  7114  fprb  7145  elunirn  7202  f1mpt  7212  isomin  7288  oprabidw  7394  oprabid  7395  mpoeq123  7435  sorpsscmpl  7684  dfwe2  7724  ssorduni  7729  ssonprc  7737  nlimsucg  7789  ordunisuc2  7791  tfinds  7807  ssnlim  7833  f1oweALT  7921  mptcnfimad  7935  el2mpocl  8032  f1o2ndf1  8068  frxp  8073  soxp  8076  poxp2  8090  poxp3  8097  poseq  8105  brtpos  8182  rntpos  8186  dftpos4  8192  onfununi  8278  onnseq  8281  smores2  8291  smo11  8301  tfr3  8335  rdglim2  8368  tz7.48lem  8377  tz7.49  8381  seqomlem2  8387  oawordex  8489  oa00  8491  oaass  8493  om00  8507  odi  8511  omass  8512  oeordi  8520  oelim2  8528  omsmo  8591  eroveu  8756  eceqoveq  8766  map0g  8829  fundmen  8975  sdomdif  9060  onsdominel  9061  pssnn  9100  nneneq  9137  php3  9140  f1finf1o  9180  findcard3  9190  unblem1  9199  fiint  9234  ixpfi2  9257  dffi2  9333  elfiun  9340  fisup2g  9379  fiinf2g  9412  wemaplem2  9459  elirrv  9509  elirrvOLD  9510  preleqALT  9536  inf3lem2  9548  inf3lem3  9549  inf3lem6  9552  noinfep  9579  epfrs  9650  tcmin  9658  r1sdom  9696  tz9.12lem3  9711  rankelb  9746  bndrank  9763  rankunb  9772  rankuni2b  9775  cplem1  9811  karden  9817  carduni  9903  infxpenlem  9933  dfac8alem  9949  alephdom  10001  cardinfima  10017  alephval3  10030  dfac5lem4  10046  dfac5lem5  10047  dfac5lem4OLD  10048  dfac5  10049  dfac2b  10051  kmlem13  10083  nnadju  10118  ackbij1b  10158  cfub  10169  coflim  10181  cflim2  10183  cfslbn  10187  cfslb2n  10188  cofsmo  10189  cfsmolem  10190  sornom  10197  fincssdom  10243  isf32lem1  10273  isf32lem2  10274  isf32lem9  10281  isf34lem4  10297  isfin1-3  10306  axcc4  10359  domtriomlem  10362  axdc2lem  10368  axdc3lem2  10371  zorn2lem4  10419  zorn2lem6  10421  zornn0g  10425  uniimadom  10464  cardmin  10484  ficard  10485  konigthlem  10489  alephreg  10503  cfpwsdom  10505  axextnd  10512  fpwwe2lem5  10556  fpwwe2lem11  10562  fpwwe2lem12  10563  fpwwe2  10564  canthp1lem2  10574  gchpwdom  10591  winalim2  10617  tskuni  10704  grupr  10718  grur1a  10740  axgroth6  10749  grothomex  10750  eltskm  10764  addclpi  10813  nqereu  10850  ltexnq  10896  nsmallnq  10898  genpn0  10924  genpss  10925  genpnmax  10928  ltaddpr  10955  reclem3pr  10970  reclem4pr  10971  suplem1pr  10973  supsrlem  11032  1re  11142  dedekindle  11308  addrid  11324  negn0  11577  negf1o  11578  negfi  12103  sup2  12110  supadd  12122  supmullem1  12124  supmullem2  12125  zmulcl  12574  zeo  12613  uz11  12811  uzwo  12859  eqreznegel  12882  lbzbi  12884  qextlt  13153  qextle  13154  xrsupsslem  13257  xrinfmsslem  13258  supxrun  13266  supxrpnf  13268  supxrunb1  13269  supxrunb2  13270  fzm1  13559  uzrdgfni  13918  hasheqf1oi  14311  hashreshashfun  14399  leisorel  14420  fundmge2nop0  14462  wrdsymb0  14509  swrdnnn0nd  14617  swrdccatin2d  14704  cshinj  14771  repswcshw  14772  rennim  15199  01sqrexlem6  15207  caubnd  15319  sqreulem  15320  caucvgrlem  15633  fsumcvg  15672  supcvg  15819  prodeq2ii  15874  fprodcvg  15893  prodmo  15899  dvdslelem  16276  bitsinv1lem  16408  bitsshft  16442  smuval2  16449  smupvallem  16450  gcdcllem1  16466  bezoutlem2  16507  bezoutlem3  16508  algcvga  16546  isprm3  16650  isprm5  16675  oddprmdvds  16872  vdwlem13  16962  vdwnnlem1  16964  vdwnnlem3  16966  ramub1lem1  16995  prmgaplem5  17024  imasaddfnlem  17490  divsfval  17509  catpropd  17673  joindmss  18341  meetdmss  18355  psdmrn  18537  odlem1  19508  gexlem1  19552  cygctb  19865  rngisomring1  20446  lmodfopnelem1  20895  islss  20931  lspsneq0  21009  lspsneq  21122  psgnodpmr  21572  obselocv  21710  mvrf1  21967  evlseu  22066  mpfrcl  22068  ppttop  22997  epttop  22999  elcls  23063  restntr  23172  cnprest  23279  regsep  23324  nrmsep3  23345  lmmo  23370  cmpsublem  23389  cmpsub  23390  hauscmplem  23396  txcnpi  23598  txcnp  23610  fbun  23830  fbfinnfr  23831  trfbas2  23833  fgcl  23868  filssufilg  23901  ufinffr  23919  isfcls  23999  fclsrest  24014  flimfnfcls  24018  alexsubALTlem2  24038  alexsubALTlem3  24039  alexsubALTlem4  24040  alexsubALT  24041  cnextcn  24057  imasf1oxms  24479  metequiv2  24500  tngngpim  24649  iccpnfcnv  24936  iccpnfhmeo  24937  iscau2  25269  caun0  25273  minveclem3b  25420  itg1climres  25706  mbfi1fseqlem4  25710  ellimc3  25871  limccnp2  25884  dvlip  25985  itgsubstlem  26040  elply2  26186  coefv0  26238  coemulc  26245  ulmss  26387  sineq0  26513  scvxcvx  26974  sqf11  27127  ppiublem1  27190  fsumvma  27201  2sq2  27421  ostth  27627  ltsres  27651  nosepdmlem  27672  nobdaymin  27770  nocvxminlem  27771  addsprop  27993  mpteleeOLD  28989  brbtwn2  28999  colinearalg  29004  axcontlem4  29061  upgrres1  29407  usgr2trlncl  29853  umgrclwwlkge2  30086  upgr4cycl4dv4e  30280  1to3vfriendship  30376  3cyclfrgrrn1  30380  n4cyclfrgr  30386  frgrncvvdeqlem8  30401  frgrwopreg  30418  2clwwlk2clwwlk  30445  numclwwlk2lem1  30471  frgrreg  30489  frgrogt3nreg  30492  nmcvcn  30791  chlimi  31330  ocsh  31379  shsvs  31419  h1datomi  31677  stcl  32312  stge0  32320  stle1  32321  stm1addi  32341  stm1add3i  32343  cvnsym  32386  mdbr2  32392  dmdbr2  32399  mdsl0  32406  mdsl1i  32417  mdsl2i  32418  cvmdi  32420  atexch  32477  atcvat4i  32493  cdj1i  32529  1arithufdlem4  33637  xrge0iifcnv  34124  esumpr2  34258  sigaclci  34323  cntmeas  34417  mbfmcnt  34459  ballotlemfc0  34684  ballotlemfcc  34685  bnj1379  35019  bnj607  35105  bnj908  35120  bnj938  35126  bnj1174  35192  bnj1280  35209  f1resrcmplf1dlem  35276  fnrelpredd  35281  r1filimi  35293  axnulg  35298  fineqvinfep  35316  tz9.1regs  35325  cusgr3cyclex  35365  loop1cycl  35366  acycgrislfgr  35381  pthacycspth  35386  iccllysconn  35479  satffunlem1lem1  35631  satfvel  35641  sate0fv0  35646  antnestlaw2  35921  funpsstri  35995  fundmpss  35996  dfon2lem3  36012  dfon2lem4  36013  dfon2lem6  36015  dfon2lem9  36018  dfon2  36019  hbimtg  36033  hbaltg  36034  dfrdg4  36180  btwntriv2  36241  btwncomim  36242  btwnswapid  36246  btwnexch3  36249  ifscgr  36273  lineunray  36376  hilbert1.2  36384  cldbnd  36555  tailfb  36606  meran3  36642  arg-ax  36645  ontopbas  36657  onsuct0  36670  limsucncmpi  36674  ordcmp  36676  onint1  36678  weiunpo  36694  axtcond  36707  axuntco  36708  dfttc4lem2  36758  bj-bisimpl  36864  bj-bisimpr  36865  bj-syl66ib  36866  bj-gl4  36907  bj-alexim  36952  bj-nfimt  36964  bj-spvw  36976  bj-cbvalvv  36980  bj-ax6e  37009  bj-hbald  37023  axc11n11r  37027  bj-nnfim  37096  bj-nnfan  37098  bj-nnfor  37100  bj-nnford  37101  bj-19.21t  37105  bj-19.23t  37106  bj-19.42t  37109  bj-sbft  37122  bj-nnflemaa  37130  bj-nnflemae  37132  bj-hbsb3t  37142  bj-cbv2hv  37151  bj-equsal1t  37176  bj-axreprepsep  37429  bj-0int  37460  bj-bary1lem1  37672  topdifinffinlem  37710  isbasisrelowllem1  37718  isbasisrelowllem2  37719  iooelexlt  37725  finorwe  37745  finxpreclem1  37752  finxpreclem2  37753  isinf2  37768  fvineqsneu  37774  fvineqsneq  37775  pibt2  37780  wl-spae  37893  wl-19.8eqv  37895  wl-nfeqfb  37908  wl-mo3t  37948  wl-eujustlem1  37960  fin2so  37975  poimirlem29  38017  poimirlem30  38018  poimirlem31  38019  poimirlem32  38020  ismblfin  38029  indexdom  38102  fzmul  38109  heibor1lem  38177  heibor  38189  exidu1  38224  rngoideu  38271  zerdivemp1x  38315  ispridl2  38406  cnf1dd  38458  cnf2dd  38459  cnfn1dd  38460  cnfn2dd  38461  orcomdd  38535  disjlem14  39269  disjdmqsss  39273  disjdmqscossss  39274  prtlem14  39367  prter2  39374  aev-o  39424  ax12eq  39434  ax12el  39435  ax12indn  39436  ax12indi  39437  lsatn0  39492  lsatcmp  39496  lsatcv0  39524  lfl1dim  39614  lfl1dim2N  39615  lkrss2N  39662  lub0N  39682  glb0N  39686  glbconxN  39871  hl2at  39898  cvrexchlem  39912  cvratlem  39914  cvrat4  39936  psubspi  40240  pointpsubN  40244  elpaddn0  40293  paddasslem17  40329  ispsubcl2N  40440  ldilval  40606  trlord  41062  diaelrnN  41538  cdlemm10N  41611  cdlemn11pre  41703  dihord2pre  41718  dihglblem2N  41787  dihglblem3N  41788  mapdrvallem2  42138  ioin9i8  42693  sn-sup2  42982  incssnn0  43161  fphpd  43262  rmxycomplete  43363  dford3lem1  43472  iocinico  43658  onsupnmax  43674  cantnfresb  43770  cantnf2  43771  tfsconcatb0  43790  tfsconcat0b  43792  sdomne0  43858  sdomne0d  43859  ensucne0OLD  43975  al3im  44092  brtrclfv2  44172  frege129d  44208  frege60a  44323  frege60c  44368  frege70  44378  rfovcnvf1od  44449  clsk1indlem3  44488  neik0pk1imk0  44492  gneispace  44579  gneispaceel2  44589  gneispacess2  44591  dvconstbi  44779  axc5c4c711toc7  44849  axc5c4c711to11  44850  pm14.24  44877  sbiota1  44879  bi33imp12  44936  bi123imp0  44941  ee233  44964  vk15.4j  44973  ssralv2  44976  alrim3con13v  44978  tratrb  44981  onfrALTlem3  44989  onfrALTlem2  44991  19.41rg  44995  hbimpg  44999  hbalg  45000  ax6e2ndeq  45004  e2  45076  ee223  45079  sspwtrALT  45266  sspwtrALT2  45267  suctrALT2  45281  trintALT  45325  isosctrlem1ALT  45378  relpmin  45397  traxext  45422  modelaxreplem2  45424  ssclaxsep  45427  fnchoice  45478  mptfnd  45687  stoweidlem62  46506  2reu8i  47577  2reuimp  47579  ffnafv  47635  lswn0  47920  reupr  47998  reuopreuprim  48002  requad2  48115  bgoldbnnsum3prm  48296  bgoldbtbndlem2  48298  bgoldbtbndlem4  48300  gricsym  48413  gpgedgvtx1  48554  ply1mulgsumlem2  48879  iunord  50167  setrec2fun  50183