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  3661  2reu1  3836  reuss2  4267  reupick2  4272  elpwunsn  4629  pwpw0  4757  sssn  4770  iuneqconst  4946  disjiun  5074  reusv1  5332  reusv3i  5339  ralxfrALT  5350  exneq  5381  opth1  5421  copsexgw  5436  copsexg  5437  opelopabt  5478  solin  5557  wefrc  5616  frinxp  5705  ssrelrn  5841  dmcosseq  5925  dmcosseqOLD  5926  reuop  6249  ordunidif  6365  oneqmini  6368  suctr  6403  ordsssuc2  6408  iotan0  6480  fv3  6850  ndmfv  6864  ssimaex  6917  fvopab3ig  6935  iinpreima  7013  fvcofneq  7037  dff3  7044  dff4  7045  ffnfv  7063  fnsnr  7109  fprb  7140  elunirn  7197  f1mpt  7207  isomin  7283  oprabidw  7389  oprabid  7390  mpoeq123  7430  sorpsscmpl  7679  dfwe2  7719  ssorduni  7724  ssonprc  7732  nlimsucg  7784  ordunisuc2  7786  tfinds  7802  ssnlim  7828  f1oweALT  7916  mptcnfimad  7930  el2mpocl  8027  f1o2ndf1  8063  frxp  8067  soxp  8070  poxp2  8084  poxp3  8091  poseq  8099  brtpos  8176  rntpos  8180  dftpos4  8186  onfununi  8272  onnseq  8275  smores2  8285  smo11  8295  tfr3  8329  rdglim2  8362  tz7.48lem  8371  tz7.49  8375  seqomlem2  8381  oawordex  8483  oa00  8485  oaass  8487  om00  8501  odi  8505  omass  8506  oeordi  8514  oelim2  8522  omsmo  8585  eroveu  8750  eceqoveq  8760  map0g  8823  fundmen  8969  sdomdif  9054  onsdominel  9055  pssnn  9094  nneneq  9131  php3  9134  f1finf1o  9174  findcard3  9184  unblem1  9193  fiint  9228  ixpfi2  9251  dffi2  9327  elfiun  9334  fisup2g  9373  fiinf2g  9406  wemaplem2  9453  elirrv  9503  preleqALT  9527  inf3lem2  9539  inf3lem3  9540  inf3lem6  9543  noinfep  9570  epfrs  9641  tcmin  9649  r1sdom  9687  tz9.12lem3  9702  rankelb  9737  bndrank  9754  rankunb  9763  rankuni2b  9766  cplem1  9802  karden  9808  carduni  9894  infxpenlem  9924  dfac8alem  9940  alephdom  9992  cardinfima  10008  alephval3  10021  dfac5lem4  10037  dfac5lem5  10038  dfac5lem4OLD  10039  dfac5  10040  dfac2b  10042  kmlem13  10074  nnadju  10109  ackbij1b  10149  cfub  10160  coflim  10172  cflim2  10174  cfslbn  10178  cfslb2n  10179  cofsmo  10180  cfsmolem  10181  sornom  10188  fincssdom  10234  isf32lem1  10264  isf32lem2  10265  isf32lem9  10272  isf34lem4  10288  isfin1-3  10297  axcc4  10350  domtriomlem  10353  axdc2lem  10359  axdc3lem2  10362  zorn2lem4  10410  zorn2lem6  10412  zornn0g  10416  uniimadom  10455  cardmin  10475  ficard  10476  konigthlem  10480  alephreg  10494  cfpwsdom  10496  axextnd  10503  fpwwe2lem5  10547  fpwwe2lem11  10553  fpwwe2lem12  10554  fpwwe2  10555  canthp1lem2  10565  gchpwdom  10582  winalim2  10608  tskuni  10695  grupr  10709  grur1a  10731  axgroth6  10740  grothomex  10741  eltskm  10755  addclpi  10804  nqereu  10841  ltexnq  10887  nsmallnq  10889  genpn0  10915  genpss  10916  genpnmax  10919  ltaddpr  10946  reclem3pr  10961  reclem4pr  10962  suplem1pr  10964  supsrlem  11023  1re  11133  dedekindle  11299  addrid  11315  negn0  11568  negf1o  11569  negfi  12094  sup2  12101  supadd  12113  supmullem1  12115  supmullem2  12116  zmulcl  12565  zeo  12604  uz11  12802  uzwo  12850  eqreznegel  12873  lbzbi  12875  qextlt  13144  qextle  13145  xrsupsslem  13248  xrinfmsslem  13249  supxrun  13257  supxrpnf  13259  supxrunb1  13260  supxrunb2  13261  fzm1  13550  uzrdgfni  13909  hasheqf1oi  14302  hashreshashfun  14390  leisorel  14411  fundmge2nop0  14453  wrdsymb0  14500  swrdnnn0nd  14608  swrdccatin2d  14695  cshinj  14762  repswcshw  14763  rennim  15190  01sqrexlem6  15198  caubnd  15310  sqreulem  15311  caucvgrlem  15624  fsumcvg  15663  supcvg  15810  prodeq2ii  15865  fprodcvg  15884  prodmo  15890  dvdslelem  16267  bitsinv1lem  16399  bitsshft  16433  smuval2  16440  smupvallem  16441  gcdcllem1  16457  bezoutlem2  16498  bezoutlem3  16499  algcvga  16537  isprm3  16641  isprm5  16666  oddprmdvds  16863  vdwlem13  16953  vdwnnlem1  16955  vdwnnlem3  16957  ramub1lem1  16986  prmgaplem5  17015  imasaddfnlem  17481  divsfval  17500  catpropd  17664  joindmss  18332  meetdmss  18346  psdmrn  18528  odlem1  19499  gexlem1  19543  cygctb  19856  rngisomring1  20437  lmodfopnelem1  20882  islss  20918  lspsneq0  20996  lspsneq  21110  psgnodpmr  21578  obselocv  21716  mvrf1  21973  evlseu  22070  mpfrcl  22072  ppttop  22981  epttop  22983  elcls  23047  restntr  23156  cnprest  23263  regsep  23308  nrmsep3  23329  lmmo  23354  cmpsublem  23373  cmpsub  23374  hauscmplem  23380  txcnpi  23582  txcnp  23594  fbun  23814  fbfinnfr  23815  trfbas2  23817  fgcl  23852  filssufilg  23885  ufinffr  23903  isfcls  23983  fclsrest  23998  flimfnfcls  24002  alexsubALTlem2  24022  alexsubALTlem3  24023  alexsubALTlem4  24024  alexsubALT  24025  cnextcn  24041  imasf1oxms  24463  metequiv2  24484  tngngpim  24633  iccpnfcnv  24920  iccpnfhmeo  24921  iscau2  25253  caun0  25257  minveclem3b  25404  itg1climres  25690  mbfi1fseqlem4  25694  ellimc3  25855  limccnp2  25868  dvlip  25970  itgsubstlem  26027  elply2  26173  coefv0  26225  coemulc  26232  ulmss  26377  sineq0  26504  scvxcvx  26967  sqf11  27120  ppiublem1  27184  fsumvma  27195  2sq2  27415  ostth  27621  ltsres  27645  nosepdmlem  27666  nobdaymin  27764  nocvxminlem  27765  addsprop  27987  mpteleeOLD  28983  brbtwn2  28993  colinearalg  28998  axcontlem4  29055  upgrres1  29401  usgr2trlncl  29848  umgrclwwlkge2  30081  upgr4cycl4dv4e  30275  1to3vfriendship  30371  3cyclfrgrrn1  30375  n4cyclfrgr  30381  frgrncvvdeqlem8  30396  frgrwopreg  30413  2clwwlk2clwwlk  30440  numclwwlk2lem1  30466  frgrreg  30484  frgrogt3nreg  30487  nmcvcn  30786  chlimi  31325  ocsh  31374  shsvs  31414  h1datomi  31672  stcl  32307  stge0  32315  stle1  32316  stm1addi  32336  stm1add3i  32338  cvnsym  32381  mdbr2  32387  dmdbr2  32394  mdsl0  32401  mdsl1i  32412  mdsl2i  32413  cvmdi  32415  atexch  32472  atcvat4i  32488  cdj1i  32524  1arithufdlem4  33627  xrge0iifcnv  34098  esumpr2  34232  sigaclci  34297  cntmeas  34391  mbfmcnt  34433  ballotlemfc0  34658  ballotlemfcc  34659  bnj1379  34993  bnj607  35079  bnj908  35094  bnj938  35100  bnj1174  35166  bnj1280  35183  f1resrcmplf1dlem  35250  fnrelpredd  35255  r1filimi  35267  axnulg  35272  fineqvinfep  35290  tz9.1regs  35299  cusgr3cyclex  35339  loop1cycl  35340  acycgrislfgr  35355  pthacycspth  35360  iccllysconn  35453  satffunlem1lem1  35605  satfvel  35615  sate0fv0  35620  antnestlaw2  35895  funpsstri  35969  fundmpss  35970  dfon2lem3  35986  dfon2lem4  35987  dfon2lem6  35989  dfon2lem9  35992  dfon2  35993  hbimtg  36007  hbaltg  36008  dfrdg4  36154  btwntriv2  36215  btwncomim  36216  btwnswapid  36220  btwnexch3  36223  ifscgr  36247  lineunray  36350  hilbert1.2  36358  cldbnd  36529  tailfb  36580  meran3  36616  arg-ax  36619  ontopbas  36631  onsuct0  36644  limsucncmpi  36648  ordcmp  36650  onint1  36652  weiunpo  36668  axtcond  36681  axuntco  36682  dfttc4lem2  36732  bj-bisimpl  36830  bj-bisimpr  36831  bj-syl66ib  36832  bj-gl4  36873  bj-alexim  36918  bj-nfimt  36930  bj-spvw  36942  bj-cbvalvv  36946  bj-ax6e  36975  bj-hbald  36989  axc11n11r  36993  bj-nnfim  37062  bj-nnfan  37064  bj-nnfor  37066  bj-nnford  37067  bj-19.21t  37071  bj-19.23t  37072  bj-19.42t  37075  bj-sbft  37088  bj-nnflemaa  37096  bj-nnflemae  37098  bj-hbsb3t  37108  bj-cbv2hv  37117  bj-equsal1t  37142  bj-axreprepsep  37395  bj-0int  37426  bj-bary1lem1  37638  topdifinffinlem  37674  isbasisrelowllem1  37682  isbasisrelowllem2  37683  iooelexlt  37689  finorwe  37709  finxpreclem1  37716  finxpreclem2  37717  isinf2  37732  fvineqsneu  37738  fvineqsneq  37739  pibt2  37744  wl-spae  37857  wl-19.8eqv  37859  wl-nfeqfb  37872  wl-mo3t  37912  wl-eujustlem1  37924  fin2so  37939  poimirlem29  37981  poimirlem30  37982  poimirlem31  37983  poimirlem32  37984  ismblfin  37993  indexdom  38066  fzmul  38073  heibor1lem  38141  heibor  38153  exidu1  38188  rngoideu  38235  zerdivemp1x  38279  ispridl2  38370  cnf1dd  38422  cnf2dd  38423  cnfn1dd  38424  cnfn2dd  38425  orcomdd  38499  disjlem14  39233  disjdmqsss  39237  disjdmqscossss  39238  prtlem14  39331  prter2  39338  aev-o  39388  ax12eq  39398  ax12el  39399  ax12indn  39400  ax12indi  39401  lsatn0  39456  lsatcmp  39460  lsatcv0  39488  lfl1dim  39578  lfl1dim2N  39579  lkrss2N  39626  lub0N  39646  glb0N  39650  glbconxN  39835  hl2at  39862  cvrexchlem  39876  cvratlem  39878  cvrat4  39900  psubspi  40204  pointpsubN  40208  elpaddn0  40257  paddasslem17  40293  ispsubcl2N  40404  ldilval  40570  trlord  41026  diaelrnN  41502  cdlemm10N  41575  cdlemn11pre  41667  dihord2pre  41682  dihglblem2N  41751  dihglblem3N  41752  mapdrvallem2  42102  ioin9i8  42657  sn-sup2  42947  incssnn0  43154  fphpd  43259  rmxycomplete  43360  dford3lem1  43469  iocinico  43655  onsupnmax  43671  cantnfresb  43767  cantnf2  43768  tfsconcatb0  43787  tfsconcat0b  43789  sdomne0  43855  sdomne0d  43856  ensucne0OLD  43972  al3im  44089  brtrclfv2  44169  frege129d  44205  frege60a  44320  frege60c  44365  frege70  44375  rfovcnvf1od  44446  clsk1indlem3  44485  neik0pk1imk0  44489  gneispace  44576  gneispaceel2  44586  gneispacess2  44588  dvconstbi  44776  axc5c4c711toc7  44846  axc5c4c711to11  44847  pm14.24  44874  sbiota1  44876  bi33imp12  44933  bi123imp0  44938  ee233  44961  vk15.4j  44970  ssralv2  44973  alrim3con13v  44975  tratrb  44978  onfrALTlem3  44986  onfrALTlem2  44988  19.41rg  44992  hbimpg  44996  hbalg  44997  ax6e2ndeq  45001  e2  45073  ee223  45076  sspwtrALT  45263  sspwtrALT2  45264  suctrALT2  45278  trintALT  45322  isosctrlem1ALT  45375  relpmin  45394  traxext  45419  modelaxreplem2  45421  ssclaxsep  45424  fnchoice  45475  mptfnd  45686  stoweidlem62  46505  2reu8i  47558  2reuimp  47560  ffnafv  47616  lswn0  47901  reupr  47979  reuopreuprim  47983  requad2  48096  bgoldbnnsum3prm  48277  bgoldbtbndlem2  48279  bgoldbtbndlem4  48281  gricsym  48394  gpgedgvtx1  48535  ply1mulgsumlem2  48860  iunord  50148  setrec2fun  50164