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  858  pm2.37  973  pm2.81  974  oplem1  1057  3jao  1428  impsingle  1629  al2im  1816  exlimdv  1935  19.23v  1944  spimfw  1967  ax13b  2034  nf5-1  2151  hbald  2174  19.8a  2189  spimedv  2205  19.9d  2211  sbequ1  2256  sbft  2277  cbv2w  2342  spimed  2393  cbv2  2408  cbv2h  2411  ax12  2428  axc11n  2431  equvini  2460  sb2  2484  sb4a  2485  mo3  2565  mopick  2626  moexexlem  2627  dvelimdc  2924  necon1ad  2950  necon4bd  2953  rsp2  3255  mo2icl  3674  2reu1  3849  reuss2  4280  reupick2  4285  elpwunsn  4643  pwpw0  4771  sssn  4784  iuneqconst  4960  disjiun  5088  reusv1  5344  reusv3i  5351  ralxfrALT  5362  exneq  5392  opth1  5431  copsexgw  5446  copsexg  5447  opelopabt  5488  solin  5567  wefrc  5626  frinxp  5715  ssrelrn  5851  dmcosseq  5935  dmcosseqOLD  5936  reuop  6259  ordunidif  6375  oneqmini  6378  suctr  6413  ordsssuc2  6418  iotan0  6490  fv3  6860  ndmfv  6874  ssimaex  6927  fvopab3ig  6945  iinpreima  7023  fvcofneq  7047  dff3  7054  dff4  7055  ffnfv  7073  fnsnr  7119  fprb  7150  elunirn  7207  f1mpt  7217  isomin  7293  oprabidw  7399  oprabid  7400  mpoeq123  7440  sorpsscmpl  7689  dfwe2  7729  ssorduni  7734  ssonprc  7742  nlimsucg  7794  ordunisuc2  7796  tfinds  7812  ssnlim  7838  f1oweALT  7926  mptcnfimad  7940  el2mpocl  8038  f1o2ndf1  8074  frxp  8078  soxp  8081  poxp2  8095  poxp3  8102  poseq  8110  brtpos  8187  rntpos  8191  dftpos4  8197  onfununi  8283  onnseq  8286  smores2  8296  smo11  8306  tfr3  8340  rdglim2  8373  tz7.48lem  8382  tz7.49  8386  seqomlem2  8392  oawordex  8494  oa00  8496  oaass  8498  om00  8512  odi  8516  omass  8517  oeordi  8525  oelim2  8533  omsmo  8596  eroveu  8761  eceqoveq  8771  map0g  8834  fundmen  8980  sdomdif  9065  onsdominel  9066  pssnn  9105  nneneq  9142  php3  9145  f1finf1o  9185  findcard3  9195  unblem1  9204  fiint  9239  ixpfi2  9262  dffi2  9338  elfiun  9345  fisup2g  9384  fiinf2g  9417  wemaplem2  9464  elirrv  9514  preleqALT  9538  inf3lem2  9550  inf3lem3  9551  inf3lem6  9554  noinfep  9581  epfrs  9652  tcmin  9660  r1sdom  9698  tz9.12lem3  9713  rankelb  9748  bndrank  9765  rankunb  9774  rankuni2b  9777  cplem1  9813  karden  9819  carduni  9905  infxpenlem  9935  dfac8alem  9951  alephdom  10003  cardinfima  10019  alephval3  10032  dfac5lem4  10048  dfac5lem5  10049  dfac5lem4OLD  10050  dfac5  10051  dfac2b  10053  kmlem13  10085  nnadju  10120  ackbij1b  10160  cfub  10171  coflim  10183  cflim2  10185  cfslbn  10189  cfslb2n  10190  cofsmo  10191  cfsmolem  10192  sornom  10199  fincssdom  10245  isf32lem1  10275  isf32lem2  10276  isf32lem9  10283  isf34lem4  10299  isfin1-3  10308  axcc4  10361  domtriomlem  10364  axdc2lem  10370  axdc3lem2  10373  zorn2lem4  10421  zorn2lem6  10423  zornn0g  10427  uniimadom  10466  cardmin  10486  ficard  10487  konigthlem  10491  alephreg  10505  cfpwsdom  10507  axextnd  10514  fpwwe2lem5  10558  fpwwe2lem11  10564  fpwwe2lem12  10565  fpwwe2  10566  canthp1lem2  10576  gchpwdom  10593  winalim2  10619  tskuni  10706  grupr  10720  grur1a  10742  axgroth6  10751  grothomex  10752  eltskm  10766  addclpi  10815  nqereu  10852  ltexnq  10898  nsmallnq  10900  genpn0  10926  genpss  10927  genpnmax  10930  ltaddpr  10957  reclem3pr  10972  reclem4pr  10973  suplem1pr  10975  supsrlem  11034  1re  11144  dedekindle  11309  addrid  11325  negn0  11578  negf1o  11579  negfi  12103  sup2  12110  supadd  12122  supmullem1  12124  supmullem2  12125  zmulcl  12552  zeo  12590  uz11  12788  uzwo  12836  eqreznegel  12859  lbzbi  12861  qextlt  13130  qextle  13131  xrsupsslem  13234  xrinfmsslem  13235  supxrun  13243  supxrpnf  13245  supxrunb1  13246  supxrunb2  13247  fzm1  13535  uzrdgfni  13893  hasheqf1oi  14286  hashreshashfun  14374  leisorel  14395  fundmge2nop0  14437  wrdsymb0  14484  swrdnnn0nd  14592  swrdccatin2d  14679  cshinj  14746  repswcshw  14747  rennim  15174  01sqrexlem6  15182  caubnd  15294  sqreulem  15295  caucvgrlem  15608  fsumcvg  15647  supcvg  15791  prodeq2ii  15846  fprodcvg  15865  prodmo  15871  dvdslelem  16248  bitsinv1lem  16380  bitsshft  16414  smuval2  16421  smupvallem  16422  gcdcllem1  16438  bezoutlem2  16479  bezoutlem3  16480  algcvga  16518  isprm3  16622  isprm5  16646  oddprmdvds  16843  vdwlem13  16933  vdwnnlem1  16935  vdwnnlem3  16937  ramub1lem1  16966  prmgaplem5  16995  imasaddfnlem  17461  divsfval  17480  catpropd  17644  joindmss  18312  meetdmss  18326  psdmrn  18508  odlem1  19476  gexlem1  19520  cygctb  19833  rngisomring1  20416  lmodfopnelem1  20861  islss  20897  lspsneq0  20975  lspsneq  21089  psgnodpmr  21557  obselocv  21695  mvrf1  21953  evlseu  22050  mpfrcl  22052  ppttop  22963  epttop  22965  elcls  23029  restntr  23138  cnprest  23245  regsep  23290  nrmsep3  23311  lmmo  23336  cmpsublem  23355  cmpsub  23356  hauscmplem  23362  txcnpi  23564  txcnp  23576  fbun  23796  fbfinnfr  23797  trfbas2  23799  fgcl  23834  filssufilg  23867  ufinffr  23885  isfcls  23965  fclsrest  23980  flimfnfcls  23984  alexsubALTlem2  24004  alexsubALTlem3  24005  alexsubALTlem4  24006  alexsubALT  24007  cnextcn  24023  imasf1oxms  24445  metequiv2  24466  tngngpim  24615  iccpnfcnv  24910  iccpnfhmeo  24911  iscau2  25245  caun0  25249  minveclem3b  25396  itg1climres  25683  mbfi1fseqlem4  25687  ellimc3  25848  limccnp2  25861  dvlip  25966  itgsubstlem  26023  elply2  26169  coefv0  26221  coemulc  26228  ulmss  26374  sineq0  26501  scvxcvx  26964  sqf11  27117  ppiublem1  27181  fsumvma  27192  2sq2  27412  ostth  27618  ltsres  27642  nosepdmlem  27663  nobdaymin  27761  nocvxminlem  27762  addsprop  27984  mpteleeOLD  28980  brbtwn2  28990  colinearalg  28995  axcontlem4  29052  upgrres1  29398  usgr2trlncl  29845  umgrclwwlkge2  30078  upgr4cycl4dv4e  30272  1to3vfriendship  30368  3cyclfrgrrn1  30372  n4cyclfrgr  30378  frgrncvvdeqlem8  30393  frgrwopreg  30410  2clwwlk2clwwlk  30437  numclwwlk2lem1  30463  frgrreg  30481  frgrogt3nreg  30484  nmcvcn  30782  chlimi  31321  ocsh  31370  shsvs  31410  h1datomi  31668  stcl  32303  stge0  32311  stle1  32312  stm1addi  32332  stm1add3i  32334  cvnsym  32377  mdbr2  32383  dmdbr2  32390  mdsl0  32397  mdsl1i  32408  mdsl2i  32409  cvmdi  32411  atexch  32468  atcvat4i  32484  cdj1i  32520  1arithufdlem4  33639  xrge0iifcnv  34110  esumpr2  34244  sigaclci  34309  cntmeas  34403  mbfmcnt  34445  ballotlemfc0  34670  ballotlemfcc  34671  bnj1379  35005  bnj607  35091  bnj908  35106  bnj938  35112  bnj1174  35178  bnj1280  35195  f1resrcmplf1dlem  35261  fnrelpredd  35266  r1filimi  35278  axnulg  35283  fineqvinfep  35300  tz9.1regs  35309  cusgr3cyclex  35349  loop1cycl  35350  acycgrislfgr  35365  pthacycspth  35370  iccllysconn  35463  satffunlem1lem1  35615  satfvel  35625  sate0fv0  35630  antnestlaw2  35905  funpsstri  35979  fundmpss  35980  dfon2lem3  35996  dfon2lem4  35997  dfon2lem6  35999  dfon2lem9  36002  dfon2  36003  hbimtg  36017  hbaltg  36018  dfrdg4  36164  btwntriv2  36225  btwncomim  36226  btwnswapid  36230  btwnexch3  36233  ifscgr  36257  lineunray  36360  hilbert1.2  36368  cldbnd  36539  tailfb  36590  meran3  36626  arg-ax  36629  ontopbas  36641  onsuct0  36654  limsucncmpi  36658  ordcmp  36660  onint1  36662  weiunpo  36678  bj-bisimpl  36774  bj-bisimpr  36775  bj-syl66ib  36776  bj-gl4  36816  bj-alexim  36854  bj-nfimt  36867  bj-spvw  36871  bj-cbvalvv  36875  bj-ax6e  36906  bj-hbalt  36919  axc11n11r  36921  bj-nnfim  36984  bj-nnfan  36986  bj-nnfor  36988  bj-nnford  36989  bj-19.21t  36995  bj-19.23t  36996  bj-19.42t  36999  bj-sbft  37009  bj-nnflemaa  37015  bj-nnflemae  37017  bj-hbsb3t  37027  bj-cbv2hv  37036  bj-equsal1t  37061  bj-axreprepsep  37314  bj-0int  37345  bj-bary1lem1  37555  topdifinffinlem  37591  isbasisrelowllem1  37599  isbasisrelowllem2  37600  iooelexlt  37606  finorwe  37626  finxpreclem1  37633  finxpreclem2  37634  isinf2  37649  fvineqsneu  37655  fvineqsneq  37656  pibt2  37661  wl-spae  37765  wl-19.8eqv  37767  wl-nfeqfb  37780  wl-mo3t  37820  wl-eujustlem1  37832  fin2so  37847  poimirlem29  37889  poimirlem30  37890  poimirlem31  37891  poimirlem32  37892  ismblfin  37901  indexdom  37974  fzmul  37981  heibor1lem  38049  heibor  38061  exidu1  38096  rngoideu  38143  zerdivemp1x  38187  ispridl2  38278  cnf1dd  38330  cnf2dd  38331  cnfn1dd  38332  cnfn2dd  38333  orcomdd  38407  disjlem14  39141  disjdmqsss  39145  disjdmqscossss  39146  prtlem14  39239  prter2  39246  aev-o  39296  ax12eq  39306  ax12el  39307  ax12indn  39308  ax12indi  39309  lsatn0  39364  lsatcmp  39368  lsatcv0  39396  lfl1dim  39486  lfl1dim2N  39487  lkrss2N  39534  lub0N  39554  glb0N  39558  glbconxN  39743  hl2at  39770  cvrexchlem  39784  cvratlem  39786  cvrat4  39808  psubspi  40112  pointpsubN  40116  elpaddn0  40165  paddasslem17  40201  ispsubcl2N  40312  ldilval  40478  trlord  40934  diaelrnN  41410  cdlemm10N  41483  cdlemn11pre  41575  dihord2pre  41590  dihglblem2N  41659  dihglblem3N  41660  mapdrvallem2  42010  ioin9i8  42566  sn-sup2  42850  incssnn0  43057  fphpd  43162  rmxycomplete  43263  dford3lem1  43372  iocinico  43558  onsupnmax  43574  cantnfresb  43670  cantnf2  43671  tfsconcatb0  43690  tfsconcat0b  43692  sdomne0  43758  sdomne0d  43759  ensucne0OLD  43875  al3im  43992  brtrclfv2  44072  frege129d  44108  frege60a  44223  frege60c  44268  frege70  44278  rfovcnvf1od  44349  clsk1indlem3  44388  neik0pk1imk0  44392  gneispace  44479  gneispaceel2  44489  gneispacess2  44491  dvconstbi  44679  axc5c4c711toc7  44749  axc5c4c711to11  44750  pm14.24  44777  sbiota1  44779  bi33imp12  44836  bi123imp0  44841  ee233  44864  vk15.4j  44873  ssralv2  44876  alrim3con13v  44878  tratrb  44881  onfrALTlem3  44889  onfrALTlem2  44891  19.41rg  44895  hbimpg  44899  hbalg  44900  ax6e2ndeq  44904  e2  44976  ee223  44979  sspwtrALT  45166  sspwtrALT2  45167  suctrALT2  45181  trintALT  45225  isosctrlem1ALT  45278  relpmin  45297  traxext  45322  modelaxreplem2  45324  ssclaxsep  45327  fnchoice  45378  mptfnd  45589  stoweidlem62  46409  2reu8i  47462  2reuimp  47464  ffnafv  47520  lswn0  47793  reupr  47871  reuopreuprim  47875  requad2  47972  bgoldbnnsum3prm  48153  bgoldbtbndlem2  48155  bgoldbtbndlem4  48157  gricsym  48270  gpgedgvtx1  48411  ply1mulgsumlem2  48736  iunord  50024  setrec2fun  50040