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  857  pm2.37  972  pm2.81  973  oplem1  1056  3jao  1427  impsingle  1628  al2im  1815  exlimdv  1934  19.23v  1943  spimfw  1966  ax13b  2033  nf5-1  2148  hbald  2171  19.8a  2184  spimedv  2200  19.9d  2206  sbequ1  2251  sbft  2272  cbv2w  2337  spimed  2388  cbv2  2403  cbv2h  2406  ax12  2423  axc11n  2426  equvini  2455  sb2  2479  sb4a  2480  mo3  2559  mopick  2620  moexexlem  2621  dvelimdc  2919  necon1ad  2945  necon4bd  2948  rsp2  3249  mo2icl  3668  2reu1  3843  reuss2  4273  reupick2  4278  elpwunsn  4634  pwpw0  4762  sssn  4775  iuneqconst  4951  disjiun  5077  reusv1  5333  reusv3i  5340  ralxfrALT  5351  exneq  5376  opth1  5413  copsexgw  5428  copsexg  5429  opelopabt  5470  solin  5549  wefrc  5608  frinxp  5697  ssrelrn  5833  dmcosseq  5916  dmcosseqOLD  5917  reuop  6240  ordunidif  6356  oneqmini  6359  suctr  6394  ordsssuc2  6399  iotan0  6471  fv3  6840  ndmfv  6854  ssimaex  6907  fvopab3ig  6925  iinpreima  7002  fvcofneq  7026  dff3  7033  dff4  7034  ffnfv  7052  fnsnr  7097  fprb  7128  elunirn  7185  f1mpt  7195  isomin  7271  oprabidw  7377  oprabid  7378  mpoeq123  7418  sorpsscmpl  7667  dfwe2  7707  ssorduni  7712  ssonprc  7720  nlimsucg  7772  ordunisuc2  7774  tfinds  7790  ssnlim  7816  f1oweALT  7904  mptcnfimad  7918  el2mpocl  8016  f1o2ndf1  8052  frxp  8056  soxp  8059  poxp2  8073  poxp3  8080  poseq  8088  brtpos  8165  rntpos  8169  dftpos4  8175  onfununi  8261  onnseq  8264  smores2  8274  smo11  8284  tfr3  8318  rdglim2  8351  tz7.48lem  8360  tz7.49  8364  seqomlem2  8370  oawordex  8472  oa00  8474  oaass  8476  om00  8490  odi  8494  omass  8495  oeordi  8502  oelim2  8510  omsmo  8573  eroveu  8736  eceqoveq  8746  map0g  8808  fundmen  8953  sdomdif  9038  onsdominel  9039  pssnn  9078  nneneq  9115  php3  9118  f1finf1o  9157  findcard3  9167  unblem1  9176  fiint  9211  ixpfi2  9234  dffi2  9307  elfiun  9314  fisup2g  9353  fiinf2g  9386  wemaplem2  9433  elirrv  9483  preleqALT  9507  inf3lem2  9519  inf3lem3  9520  inf3lem6  9523  noinfep  9550  epfrs  9621  tcmin  9629  r1sdom  9667  tz9.12lem3  9682  rankelb  9717  bndrank  9734  rankunb  9743  rankuni2b  9746  cplem1  9782  karden  9788  carduni  9874  infxpenlem  9904  dfac8alem  9920  alephdom  9972  cardinfima  9988  alephval3  10001  dfac5lem4  10017  dfac5lem5  10018  dfac5lem4OLD  10019  dfac5  10020  dfac2b  10022  kmlem13  10054  nnadju  10089  ackbij1b  10129  cfub  10140  coflim  10152  cflim2  10154  cfslbn  10158  cfslb2n  10159  cofsmo  10160  cfsmolem  10161  sornom  10168  fincssdom  10214  isf32lem1  10244  isf32lem2  10245  isf32lem9  10252  isf34lem4  10268  isfin1-3  10277  axcc4  10330  domtriomlem  10333  axdc2lem  10339  axdc3lem2  10342  zorn2lem4  10390  zorn2lem6  10392  zornn0g  10396  uniimadom  10435  cardmin  10455  ficard  10456  konigthlem  10459  alephreg  10473  cfpwsdom  10475  axextnd  10482  fpwwe2lem5  10526  fpwwe2lem11  10532  fpwwe2lem12  10533  fpwwe2  10534  canthp1lem2  10544  gchpwdom  10561  winalim2  10587  tskuni  10674  grupr  10688  grur1a  10710  axgroth6  10719  grothomex  10720  eltskm  10734  addclpi  10783  nqereu  10820  ltexnq  10866  nsmallnq  10868  genpn0  10894  genpss  10895  genpnmax  10898  ltaddpr  10925  reclem3pr  10940  reclem4pr  10941  suplem1pr  10943  supsrlem  11002  1re  11112  dedekindle  11277  addrid  11293  negn0  11546  negf1o  11547  negfi  12071  sup2  12078  supadd  12090  supmullem1  12092  supmullem2  12093  zmulcl  12521  zeo  12559  uz11  12757  uzwo  12809  eqreznegel  12832  lbzbi  12834  qextlt  13102  qextle  13103  xrsupsslem  13206  xrinfmsslem  13207  supxrun  13215  supxrpnf  13217  supxrunb1  13218  supxrunb2  13219  fzm1  13507  uzrdgfni  13865  hasheqf1oi  14258  hashreshashfun  14346  leisorel  14367  fundmge2nop0  14409  wrdsymb0  14456  swrdnnn0nd  14564  swrdccatin2d  14651  cshinj  14718  repswcshw  14719  rennim  15146  01sqrexlem6  15154  caubnd  15266  sqreulem  15267  caucvgrlem  15580  fsumcvg  15619  supcvg  15763  prodeq2ii  15818  fprodcvg  15837  prodmo  15843  dvdslelem  16220  bitsinv1lem  16352  bitsshft  16386  smuval2  16393  smupvallem  16394  gcdcllem1  16410  bezoutlem2  16451  bezoutlem3  16452  algcvga  16490  isprm3  16594  isprm5  16618  oddprmdvds  16815  vdwlem13  16905  vdwnnlem1  16907  vdwnnlem3  16909  ramub1lem1  16938  prmgaplem5  16967  imasaddfnlem  17432  divsfval  17451  catpropd  17615  joindmss  18283  meetdmss  18297  psdmrn  18479  odlem1  19447  gexlem1  19491  cygctb  19804  rngisomring1  20386  lmodfopnelem1  20831  islss  20867  lspsneq0  20945  lspsneq  21059  psgnodpmr  21527  obselocv  21665  mvrf1  21923  evlseu  22018  mpfrcl  22020  ppttop  22922  epttop  22924  elcls  22988  restntr  23097  cnprest  23204  regsep  23249  nrmsep3  23270  lmmo  23295  cmpsublem  23314  cmpsub  23315  hauscmplem  23321  txcnpi  23523  txcnp  23535  fbun  23755  fbfinnfr  23756  trfbas2  23758  fgcl  23793  filssufilg  23826  ufinffr  23844  isfcls  23924  fclsrest  23939  flimfnfcls  23943  alexsubALTlem2  23963  alexsubALTlem3  23964  alexsubALTlem4  23965  alexsubALT  23966  cnextcn  23982  imasf1oxms  24404  metequiv2  24425  tngngpim  24574  iccpnfcnv  24869  iccpnfhmeo  24870  iscau2  25204  caun0  25208  minveclem3b  25355  itg1climres  25642  mbfi1fseqlem4  25646  ellimc3  25807  limccnp2  25820  dvlip  25925  itgsubstlem  25982  elply2  26128  coefv0  26180  coemulc  26187  ulmss  26333  sineq0  26460  scvxcvx  26923  sqf11  27076  ppiublem1  27140  fsumvma  27151  2sq2  27371  ostth  27577  sltres  27601  nosepdmlem  27622  nobdaymin  27716  nocvxminlem  27717  addsprop  27919  mptelee  28873  brbtwn2  28883  colinearalg  28888  axcontlem4  28945  upgrres1  29291  usgr2trlncl  29738  umgrclwwlkge2  29971  upgr4cycl4dv4e  30165  1to3vfriendship  30261  3cyclfrgrrn1  30265  n4cyclfrgr  30271  frgrncvvdeqlem8  30286  frgrwopreg  30303  2clwwlk2clwwlk  30330  numclwwlk2lem1  30356  frgrreg  30374  frgrogt3nreg  30377  nmcvcn  30675  chlimi  31214  ocsh  31263  shsvs  31303  h1datomi  31561  stcl  32196  stge0  32204  stle1  32205  stm1addi  32225  stm1add3i  32227  cvnsym  32270  mdbr2  32276  dmdbr2  32283  mdsl0  32290  mdsl1i  32301  mdsl2i  32302  cvmdi  32304  atexch  32361  atcvat4i  32377  cdj1i  32413  1arithufdlem4  33512  xrge0iifcnv  33946  esumpr2  34080  sigaclci  34145  cntmeas  34239  mbfmcnt  34281  ballotlemfc0  34506  ballotlemfcc  34507  bnj1379  34842  bnj607  34928  bnj908  34943  bnj938  34949  bnj1174  35015  bnj1280  35032  f1resrcmplf1dlem  35098  fnrelpredd  35102  r1filimi  35114  axnulg  35119  tz9.1regs  35130  cusgr3cyclex  35180  loop1cycl  35181  acycgrislfgr  35196  pthacycspth  35201  iccllysconn  35294  satffunlem1lem1  35446  satfvel  35456  sate0fv0  35461  antnestlaw2  35736  funpsstri  35810  fundmpss  35811  dfon2lem3  35827  dfon2lem4  35828  dfon2lem6  35830  dfon2lem9  35833  dfon2  35834  hbimtg  35848  hbaltg  35849  dfrdg4  35995  btwntriv2  36056  btwncomim  36057  btwnswapid  36061  btwnexch3  36064  ifscgr  36088  lineunray  36191  hilbert1.2  36199  cldbnd  36370  tailfb  36421  meran3  36457  arg-ax  36460  ontopbas  36472  onsuct0  36485  limsucncmpi  36489  ordcmp  36491  onint1  36493  weiunpo  36509  bj-syl66ib  36599  bj-gl4  36639  bj-alexim  36671  bj-nfimt  36682  bj-ax6e  36712  bj-hbalt  36725  axc11n11r  36727  bj-nnfim  36790  bj-nnfan  36792  bj-nnfor  36794  bj-nnford  36795  bj-nnflemaa  36806  bj-nnflemae  36808  bj-19.21t  36813  bj-19.23t  36814  bj-19.42t  36817  bj-sbft  36819  bj-hbsb3t  36832  bj-cbv2hv  36841  bj-equsal1t  36866  bj-0int  37145  bj-bary1lem1  37355  topdifinffinlem  37391  isbasisrelowllem1  37399  isbasisrelowllem2  37400  iooelexlt  37406  finorwe  37426  finxpreclem1  37433  finxpreclem2  37434  isinf2  37449  fvineqsneu  37455  fvineqsneq  37456  pibt2  37461  wl-spae  37565  wl-19.8eqv  37567  wl-nfeqfb  37580  wl-mo3t  37620  fin2so  37646  poimirlem29  37688  poimirlem30  37689  poimirlem31  37690  poimirlem32  37691  ismblfin  37700  indexdom  37773  fzmul  37780  heibor1lem  37848  heibor  37860  exidu1  37895  rngoideu  37942  zerdivemp1x  37986  ispridl2  38077  cnf1dd  38129  cnf2dd  38130  cnfn1dd  38131  cnfn2dd  38132  orcomdd  38206  disjlem14  38895  disjdmqsss  38899  disjdmqscossss  38900  prtlem14  38972  prter2  38979  aev-o  39029  ax12eq  39039  ax12el  39040  ax12indn  39041  ax12indi  39042  lsatn0  39097  lsatcmp  39101  lsatcv0  39129  lfl1dim  39219  lfl1dim2N  39220  lkrss2N  39267  lub0N  39287  glb0N  39291  glbconxN  39476  hl2at  39503  cvrexchlem  39517  cvratlem  39519  cvrat4  39541  psubspi  39845  pointpsubN  39849  elpaddn0  39898  paddasslem17  39934  ispsubcl2N  40045  ldilval  40211  trlord  40667  diaelrnN  41143  cdlemm10N  41216  cdlemn11pre  41308  dihord2pre  41323  dihglblem2N  41392  dihglblem3N  41393  mapdrvallem2  41743  ioin9i8  42299  sn-sup2  42583  incssnn0  42803  fphpd  42908  rmxycomplete  43009  dford3lem1  43118  iocinico  43304  onsupnmax  43320  cantnfresb  43416  cantnf2  43417  tfsconcatb0  43436  tfsconcat0b  43438  sdomne0  43505  sdomne0d  43506  ensucne0OLD  43622  al3im  43739  brtrclfv2  43819  frege129d  43855  frege60a  43970  frege60c  44015  frege70  44025  rfovcnvf1od  44096  clsk1indlem3  44135  neik0pk1imk0  44139  gneispace  44226  gneispaceel2  44236  gneispacess2  44238  dvconstbi  44426  axc5c4c711toc7  44496  axc5c4c711to11  44497  pm14.24  44524  sbiota1  44526  bi33imp12  44583  bi123imp0  44588  ee233  44611  vk15.4j  44620  ssralv2  44623  alrim3con13v  44625  tratrb  44628  onfrALTlem3  44636  onfrALTlem2  44638  19.41rg  44642  hbimpg  44646  hbalg  44647  ax6e2ndeq  44651  e2  44723  ee223  44726  sspwtrALT  44913  sspwtrALT2  44914  suctrALT2  44928  trintALT  44972  isosctrlem1ALT  45025  relpmin  45044  traxext  45069  modelaxreplem2  45071  ssclaxsep  45074  fnchoice  45125  mptfnd  45338  stoweidlem62  46159  2reu8i  47212  2reuimp  47214  ffnafv  47270  lswn0  47543  reupr  47621  reuopreuprim  47625  requad2  47722  bgoldbnnsum3prm  47903  bgoldbtbndlem2  47905  bgoldbtbndlem4  47907  gricsym  48020  gpgedgvtx1  48161  ply1mulgsumlem2  48487  iunord  49776  setrec2fun  49792