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  1426  impsingle  1626  al2im  1813  exlimdv  1932  19.23v  1941  spimfw  1964  ax13b  2030  nf5-1  2144  hbald  2167  19.8a  2180  spimedv  2196  19.9d  2202  sbequ1  2247  sbft  2269  cbv2w  2337  spimed  2391  cbv2  2406  cbv2h  2409  ax12  2426  axc11n  2429  equvini  2458  sb2  2482  sb4a  2483  mo3  2562  mopick  2623  moexexlem  2624  dvelimdc  2922  necon1ad  2948  necon4bd  2951  rsp2  3263  mo2icl  3704  2reu1  3879  reuss2  4308  reupick2  4313  elpwunsn  4666  pwpw0  4795  sssn  4808  iuneqconst  4985  disjiun  5113  reusv1  5379  reusv3i  5386  ralxfrALT  5397  exneq  5422  opth1  5462  copsexgw  5477  copsexg  5478  opelopabt  5519  solin  5601  wefrc  5661  frinxp  5750  ssrelrn  5887  dmcosseq  5969  reuop  6295  ordunidif  6414  oneqmini  6417  suctr  6451  ordsssuc2  6456  iotan0  6532  fv3  6905  ndmfv  6922  ssimaex  6975  fvopab3ig  6993  iinpreima  7070  fvcofneq  7094  dff3  7101  dff4  7102  ffnfv  7120  fnsnr  7166  fprb  7197  elunirn  7254  f1mpt  7264  isomin  7340  oprabidw  7445  oprabid  7446  mpoeq123  7488  sorpsscmpl  7737  dfwe2  7777  ssorduni  7782  ssonprc  7790  nlimsucg  7846  ordunisuc2  7848  tfinds  7864  ssnlim  7890  f1oweALT  7980  mptcnfimad  7994  el2mpocl  8094  f1o2ndf1  8130  frxp  8134  soxp  8137  poxp2  8151  poxp3  8158  poseq  8166  brtpos  8243  rntpos  8247  dftpos4  8253  onfununi  8364  onnseq  8367  smores2  8377  smo11  8387  tfr3  8422  rdglim2  8455  tz7.48lem  8464  tz7.49  8468  seqomlem2  8474  oawordex  8578  oa00  8580  oaass  8582  om00  8596  odi  8600  omass  8601  oeordi  8608  oelim2  8616  omsmo  8679  eroveu  8835  eceqoveq  8845  map0g  8907  fundmen  9054  sdomdif  9148  onsdominel  9149  pssnn  9191  nneneq  9229  php3  9232  nneneqOLD  9241  php3OLD  9244  onomeneqOLD  9249  f1finf1o  9288  f1finf1oOLD  9289  findcard3  9301  findcard3OLD  9302  unblem1  9311  fiint  9349  fiintOLD  9350  ixpfi2  9373  dffi2  9446  elfiun  9453  fisup2g  9491  fiinf2g  9523  wemaplem2  9570  preleqALT  9640  inf3lem2  9652  inf3lem3  9653  inf3lem6  9656  noinfep  9683  epfrs  9754  tcmin  9764  r1sdom  9797  tz9.12lem3  9812  rankelb  9847  bndrank  9864  rankunb  9873  rankuni2b  9876  cplem1  9912  karden  9918  carduni  10004  infxpenlem  10036  dfac8alem  10052  alephdom  10104  cardinfima  10120  alephval3  10133  dfac5lem4  10149  dfac5lem5  10150  dfac5lem4OLD  10151  dfac5  10152  dfac2b  10154  kmlem13  10186  nnadju  10221  ackbij1b  10261  cfub  10272  coflim  10284  cflim2  10286  cfslbn  10290  cfslb2n  10291  cofsmo  10292  cfsmolem  10293  sornom  10300  fincssdom  10346  isf32lem1  10376  isf32lem2  10377  isf32lem9  10384  isf34lem4  10400  isfin1-3  10409  axcc4  10462  domtriomlem  10465  axdc2lem  10471  axdc3lem2  10474  zorn2lem4  10522  zorn2lem6  10524  zornn0g  10528  uniimadom  10567  cardmin  10587  ficard  10588  konigthlem  10591  alephreg  10605  cfpwsdom  10607  axextnd  10614  fpwwe2lem5  10658  fpwwe2lem11  10664  fpwwe2lem12  10665  fpwwe2  10666  canthp1lem2  10676  gchpwdom  10693  winalim2  10719  tskuni  10806  grupr  10820  grur1a  10842  axgroth6  10851  grothomex  10852  eltskm  10866  addclpi  10915  nqereu  10952  ltexnq  10998  nsmallnq  11000  genpn0  11026  genpss  11027  genpnmax  11030  ltaddpr  11057  reclem3pr  11072  reclem4pr  11073  suplem1pr  11075  supsrlem  11134  1re  11244  dedekindle  11408  addrid  11424  negn0  11675  negf1o  11676  negfi  12200  sup2  12207  supadd  12219  supmullem1  12221  supmullem2  12222  zmulcl  12650  zeo  12688  uz11  12886  uzwo  12936  eqreznegel  12959  lbzbi  12961  qextlt  13228  qextle  13229  xrsupsslem  13332  xrinfmsslem  13333  supxrun  13341  supxrpnf  13343  supxrunb1  13344  supxrunb2  13345  fzm1  13630  uzrdgfni  13982  hasheqf1oi  14373  hashreshashfun  14461  leisorel  14482  fundmge2nop0  14524  wrdsymb0  14570  swrdnnn0nd  14677  swrdccatin2d  14765  cshinj  14832  repswcshw  14833  rennim  15261  01sqrexlem6  15269  caubnd  15380  sqreulem  15381  caucvgrlem  15692  fsumcvg  15731  supcvg  15875  prodeq2ii  15930  fprodcvg  15949  prodmo  15955  dvdslelem  16329  bitsinv1lem  16461  bitsshft  16495  smuval2  16502  smupvallem  16503  gcdcllem1  16519  bezoutlem2  16560  bezoutlem3  16561  algcvga  16599  isprm3  16703  isprm5  16727  oddprmdvds  16924  vdwlem13  17014  vdwnnlem1  17016  vdwnnlem3  17018  ramub1lem1  17047  prmgaplem5  17076  imasaddfnlem  17549  divsfval  17568  catpropd  17728  joindmss  18398  meetdmss  18412  psdmrn  18592  odlem1  19526  gexlem1  19570  cygctb  19883  rngisomring1  20441  lmodfopnelem1  20869  islss  20905  lspsneq0  20983  lspsneq  21097  psgnodpmr  21575  obselocv  21715  mvrf1  21973  evlseu  22074  mpfrcl  22076  ppttop  22980  epttop  22982  elcls  23046  restntr  23155  cnprest  23262  regsep  23307  nrmsep3  23328  lmmo  23353  cmpsublem  23372  cmpsub  23373  hauscmplem  23379  txcnpi  23581  txcnp  23593  fbun  23813  fbfinnfr  23814  trfbas2  23816  fgcl  23851  filssufilg  23884  ufinffr  23902  isfcls  23982  fclsrest  23997  flimfnfcls  24001  alexsubALTlem2  24021  alexsubALTlem3  24022  alexsubALTlem4  24023  alexsubALT  24024  cnextcn  24040  imasf1oxms  24465  metequiv2  24486  tngngpim  24635  iccpnfcnv  24930  iccpnfhmeo  24931  iscau2  25266  caun0  25270  minveclem3b  25417  itg1climres  25704  mbfi1fseqlem4  25708  ellimc3  25869  limccnp2  25882  dvlip  25987  itgsubstlem  26044  elply2  26190  coefv0  26242  coemulc  26249  ulmss  26395  sineq0  26521  scvxcvx  26984  sqf11  27137  ppiublem1  27201  fsumvma  27212  2sq2  27432  ostth  27638  sltres  27662  nosepdmlem  27683  nocvxminlem  27777  nocvxmin  27778  addsprop  27964  mptelee  28859  brbtwn2  28869  colinearalg  28874  axcontlem4  28931  upgrres1  29277  usgr2trlncl  29727  umgrclwwlkge2  29957  upgr4cycl4dv4e  30151  1to3vfriendship  30247  3cyclfrgrrn1  30251  n4cyclfrgr  30257  frgrncvvdeqlem8  30272  frgrwopreg  30289  2clwwlk2clwwlk  30316  numclwwlk2lem1  30342  frgrreg  30360  frgrogt3nreg  30363  nmcvcn  30661  chlimi  31200  ocsh  31249  shsvs  31289  h1datomi  31547  stcl  32182  stge0  32190  stle1  32191  stm1addi  32211  stm1add3i  32213  cvnsym  32256  mdbr2  32262  dmdbr2  32269  mdsl0  32276  mdsl1i  32287  mdsl2i  32288  cvmdi  32290  atexch  32347  atcvat4i  32363  cdj1i  32399  1arithufdlem4  33516  xrge0iifcnv  33873  esumpr2  34009  sigaclci  34074  cntmeas  34168  mbfmcnt  34211  ballotlemfc0  34436  ballotlemfcc  34437  bnj1379  34785  bnj607  34871  bnj908  34886  bnj938  34892  bnj1174  34958  bnj1280  34975  f1resrcmplf1dlem  35041  fnrelpredd  35044  axnulg  35047  cusgr3cyclex  35082  loop1cycl  35083  acycgrislfgr  35098  pthacycspth  35103  iccllysconn  35196  satffunlem1lem1  35348  satfvel  35358  sate0fv0  35363  funpsstri  35707  fundmpss  35708  dfon2lem3  35727  dfon2lem4  35728  dfon2lem6  35730  dfon2lem9  35733  dfon2  35734  hbimtg  35748  hbaltg  35749  dfrdg4  35893  btwntriv2  35954  btwncomim  35955  btwnswapid  35959  btwnexch3  35962  ifscgr  35986  lineunray  36089  hilbert1.2  36097  cldbnd  36268  tailfb  36319  meran3  36355  arg-ax  36358  ontopbas  36370  onsuct0  36383  limsucncmpi  36387  ordcmp  36389  onint1  36391  weiunpo  36407  bj-syl66ib  36497  bj-gl4  36537  bj-alexim  36569  bj-nfimt  36580  bj-ax6e  36610  bj-hbalt  36623  axc11n11r  36625  bj-nnfim  36688  bj-nnfan  36690  bj-nnfor  36692  bj-nnford  36693  bj-nnflemaa  36704  bj-nnflemae  36706  bj-19.21t  36711  bj-19.23t  36712  bj-19.42t  36715  bj-sbft  36717  bj-hbsb3t  36730  bj-cbv2hv  36739  bj-equsal1t  36764  bj-0int  37043  bj-bary1lem1  37253  topdifinffinlem  37289  isbasisrelowllem1  37297  isbasisrelowllem2  37298  iooelexlt  37304  finorwe  37324  finxpreclem1  37331  finxpreclem2  37332  isinf2  37347  fvineqsneu  37353  fvineqsneq  37354  pibt2  37359  wl-spae  37463  wl-19.8eqv  37465  wl-nfeqfb  37478  wl-mo3t  37518  wl-ax11-lem3  37529  fin2so  37555  poimirlem29  37597  poimirlem30  37598  poimirlem31  37599  poimirlem32  37600  ismblfin  37609  indexdom  37682  fzmul  37689  heibor1lem  37757  heibor  37769  exidu1  37804  rngoideu  37851  zerdivemp1x  37895  ispridl2  37986  cnf1dd  38038  cnf2dd  38039  cnfn1dd  38040  cnfn2dd  38041  orcomdd  38115  disjlem14  38740  disjdmqsss  38744  disjdmqscossss  38745  prtlem14  38816  prter2  38823  aev-o  38873  ax12eq  38883  ax12el  38884  ax12indn  38885  ax12indi  38886  lsatn0  38941  lsatcmp  38945  lsatcv0  38973  lfl1dim  39063  lfl1dim2N  39064  lkrss2N  39111  lub0N  39131  glb0N  39135  glbconxN  39321  hl2at  39348  cvrexchlem  39362  cvratlem  39364  cvrat4  39386  psubspi  39690  pointpsubN  39694  elpaddn0  39743  paddasslem17  39779  ispsubcl2N  39890  ldilval  40056  trlord  40512  diaelrnN  40988  cdlemm10N  41061  cdlemn11pre  41153  dihord2pre  41168  dihglblem2N  41237  dihglblem3N  41238  mapdrvallem2  41588  ioin9i8  42187  sn-sup2  42446  incssnn0  42667  fphpd  42772  rmxycomplete  42874  dford3lem1  42983  iocinico  43169  onsupnmax  43185  cantnfresb  43282  cantnf2  43283  tfsconcatb0  43302  tfsconcat0b  43304  sdomne0  43371  sdomne0d  43372  ensucne0OLD  43488  al3im  43605  brtrclfv2  43685  frege129d  43721  frege60a  43836  frege60c  43881  frege70  43891  rfovcnvf1od  43962  clsk1indlem3  44001  neik0pk1imk0  44005  gneispace  44092  gneispaceel2  44102  gneispacess2  44104  dvconstbi  44298  axc5c4c711toc7  44368  axc5c4c711to11  44369  pm14.24  44396  sbiota1  44398  bi33imp12  44456  bi123imp0  44461  ee233  44484  vk15.4j  44493  ssralv2  44496  alrim3con13v  44498  tratrb  44501  onfrALTlem3  44509  onfrALTlem2  44511  19.41rg  44515  hbimpg  44519  hbalg  44520  ax6e2ndeq  44524  e2  44596  ee223  44599  sspwtrALT  44787  sspwtrALT2  44788  suctrALT2  44802  trintALT  44846  isosctrlem1ALT  44899  relpmin  44918  traxext  44939  modelaxreplem2  44941  ssclaxsep  44944  fnchoice  44979  mptfnd  45193  stoweidlem62  46022  2reu8i  47071  2reuimp  47073  ffnafv  47129  lswn0  47377  reupr  47455  reuopreuprim  47459  requad2  47556  bgoldbnnsum3prm  47737  bgoldbtbndlem2  47739  bgoldbtbndlem4  47741  gricsym  47836  gpgedgvtx1  47966  ply1mulgsumlem2  48250  iunord  49191  setrec2fun  49207