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  trun  5204  reusv1  5340  reusv3i  5347  ralxfrALT  5358  exneq  5389  opth1  5429  copsexgwOLD  5445  copsexg  5446  opelopabt  5487  solin  5566  wefrc  5625  frinxp  5714  ssrelrn  5850  dmcosseq  5934  dmcosseqOLD  5935  reuop  6258  ordunidif  6374  oneqmini  6377  suctr  6412  ordsssuc2  6417  iotan0  6489  fv3  6859  ndmfv  6873  ssimaex  6926  fvopab3ig  6944  iinpreima  7022  fvcofneq  7046  dff3  7053  dff4  7054  ffnfv  7072  fnsnr  7118  fprb  7149  elunirn  7206  f1mpt  7216  isomin  7292  oprabidw  7398  oprabid  7399  mpoeq123  7439  sorpsscmpl  7688  dfwe2  7728  ssorduni  7733  ssonprc  7741  nlimsucg  7793  ordunisuc2  7795  tfinds  7811  ssnlim  7837  f1oweALT  7925  mptcnfimad  7939  el2mpocl  8036  f1o2ndf1  8072  frxp  8076  soxp  8079  poxp2  8093  poxp3  8100  poseq  8108  brtpos  8185  rntpos  8189  dftpos4  8195  onfununi  8281  onnseq  8284  smores2  8294  smo11  8304  tfr3  8338  rdglim2  8371  tz7.48lem  8380  tz7.49  8384  seqomlem2  8390  oawordex  8492  oa00  8494  oaass  8496  om00  8510  odi  8514  omass  8515  oeordi  8523  oelim2  8531  omsmo  8594  eroveu  8759  eceqoveq  8769  map0g  8832  fundmen  8978  sdomdif  9063  onsdominel  9064  pssnn  9103  nneneq  9140  php3  9143  f1finf1o  9183  findcard3  9193  unblem1  9202  fiint  9237  ixpfi2  9260  dffi2  9336  elfiun  9343  fisup2g  9382  fiinf2g  9415  wemaplem2  9462  elirrv  9512  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  11310  addrid  11326  negn0  11579  negf1o  11580  negfi  12105  sup2  12112  supadd  12124  supmullem1  12126  supmullem2  12127  zmulcl  12576  zeo  12615  uz11  12813  uzwo  12861  eqreznegel  12884  lbzbi  12886  qextlt  13155  qextle  13156  xrsupsslem  13259  xrinfmsslem  13260  supxrun  13268  supxrpnf  13270  supxrunb1  13271  supxrunb2  13272  fzm1  13561  uzrdgfni  13920  hasheqf1oi  14313  hashreshashfun  14401  leisorel  14422  fundmge2nop0  14464  wrdsymb0  14511  swrdnnn0nd  14619  swrdccatin2d  14706  cshinj  14773  repswcshw  14774  rennim  15201  01sqrexlem6  15209  caubnd  15321  sqreulem  15322  caucvgrlem  15635  fsumcvg  15674  supcvg  15821  prodeq2ii  15876  fprodcvg  15895  prodmo  15901  dvdslelem  16278  bitsinv1lem  16410  bitsshft  16444  smuval2  16451  smupvallem  16452  gcdcllem1  16468  bezoutlem2  16509  bezoutlem3  16510  algcvga  16548  isprm3  16652  isprm5  16677  oddprmdvds  16874  vdwlem13  16964  vdwnnlem1  16966  vdwnnlem3  16968  ramub1lem1  16997  prmgaplem5  17026  imasaddfnlem  17492  divsfval  17511  catpropd  17675  joindmss  18343  meetdmss  18357  psdmrn  18539  odlem1  19510  gexlem1  19554  cygctb  19867  rngisomring1  20448  lmodfopnelem1  20893  islss  20929  lspsneq0  21007  lspsneq  21120  psgnodpmr  21570  obselocv  21708  mvrf1  21964  evlseu  22061  mpfrcl  22063  ppttop  22972  epttop  22974  elcls  23038  restntr  23147  cnprest  23254  regsep  23299  nrmsep3  23320  lmmo  23345  cmpsublem  23364  cmpsub  23365  hauscmplem  23371  txcnpi  23573  txcnp  23585  fbun  23805  fbfinnfr  23806  trfbas2  23808  fgcl  23843  filssufilg  23876  ufinffr  23894  isfcls  23974  fclsrest  23989  flimfnfcls  23993  alexsubALTlem2  24013  alexsubALTlem3  24014  alexsubALTlem4  24015  alexsubALT  24016  cnextcn  24032  imasf1oxms  24454  metequiv2  24475  tngngpim  24624  iccpnfcnv  24911  iccpnfhmeo  24912  iscau2  25244  caun0  25248  minveclem3b  25395  itg1climres  25681  mbfi1fseqlem4  25685  ellimc3  25846  limccnp2  25859  dvlip  25960  itgsubstlem  26015  elply2  26161  coefv0  26213  coemulc  26220  ulmss  26362  sineq0  26488  scvxcvx  26949  sqf11  27102  ppiublem1  27165  fsumvma  27176  2sq2  27396  ostth  27602  ltsres  27626  nosepdmlem  27647  nobdaymin  27745  nocvxminlem  27746  addsprop  27968  mpteleeOLD  28964  brbtwn2  28974  colinearalg  28979  axcontlem4  29036  upgrres1  29382  usgr2trlncl  29828  umgrclwwlkge2  30061  upgr4cycl4dv4e  30255  1to3vfriendship  30351  3cyclfrgrrn1  30355  n4cyclfrgr  30361  frgrncvvdeqlem8  30376  frgrwopreg  30393  2clwwlk2clwwlk  30420  numclwwlk2lem1  30446  frgrreg  30464  frgrogt3nreg  30467  nmcvcn  30766  chlimi  31305  ocsh  31354  shsvs  31394  h1datomi  31652  stcl  32287  stge0  32295  stle1  32296  stm1addi  32316  stm1add3i  32318  cvnsym  32361  mdbr2  32367  dmdbr2  32374  mdsl0  32381  mdsl1i  32392  mdsl2i  32393  cvmdi  32395  atexch  32452  atcvat4i  32468  cdj1i  32504  1arithufdlem4  33607  xrge0iifcnv  34077  esumpr2  34211  sigaclci  34276  cntmeas  34370  mbfmcnt  34412  ballotlemfc0  34637  ballotlemfcc  34638  bnj1379  34972  bnj607  35058  bnj908  35073  bnj938  35079  bnj1174  35145  bnj1280  35162  f1resrcmplf1dlem  35229  fnrelpredd  35234  r1filimi  35246  axnulg  35251  fineqvinfep  35269  tz9.1regs  35278  cusgr3cyclex  35318  loop1cycl  35319  acycgrislfgr  35334  pthacycspth  35339  iccllysconn  35432  satffunlem1lem1  35584  satfvel  35594  sate0fv0  35599  antnestlaw2  35874  funpsstri  35948  fundmpss  35949  dfon2lem3  35965  dfon2lem4  35966  dfon2lem6  35968  dfon2lem9  35971  dfon2  35972  hbimtg  35986  hbaltg  35987  dfrdg4  36133  btwntriv2  36194  btwncomim  36195  btwnswapid  36199  btwnexch3  36202  ifscgr  36226  lineunray  36329  hilbert1.2  36337  cldbnd  36508  tailfb  36559  meran3  36595  arg-ax  36598  ontopbas  36610  onsuct0  36623  limsucncmpi  36627  ordcmp  36629  onint1  36631  weiunpo  36647  axtcond  36660  axuntco  36661  dfttc4lem2  36711  bj-bisimpl  36817  bj-bisimpr  36818  bj-syl66ib  36819  bj-gl4  36860  bj-alexim  36905  bj-nfimt  36917  bj-spvw  36929  bj-cbvalvv  36933  bj-ax6e  36962  bj-hbald  36976  axc11n11r  36980  bj-nnfim  37049  bj-nnfan  37051  bj-nnfor  37053  bj-nnford  37054  bj-19.21t  37058  bj-19.23t  37059  bj-19.42t  37062  bj-sbft  37075  bj-nnflemaa  37083  bj-nnflemae  37085  bj-hbsb3t  37095  bj-cbv2hv  37104  bj-equsal1t  37129  bj-axreprepsep  37382  bj-0int  37413  bj-bary1lem1  37625  topdifinffinlem  37663  isbasisrelowllem1  37671  isbasisrelowllem2  37672  iooelexlt  37678  finorwe  37698  finxpreclem1  37705  finxpreclem2  37706  isinf2  37721  fvineqsneu  37727  fvineqsneq  37728  pibt2  37733  wl-spae  37846  wl-19.8eqv  37848  wl-nfeqfb  37861  wl-mo3t  37901  wl-eujustlem1  37913  fin2so  37928  poimirlem29  37970  poimirlem30  37971  poimirlem31  37972  poimirlem32  37973  ismblfin  37982  indexdom  38055  fzmul  38062  heibor1lem  38130  heibor  38142  exidu1  38177  rngoideu  38224  zerdivemp1x  38268  ispridl2  38359  cnf1dd  38411  cnf2dd  38412  cnfn1dd  38413  cnfn2dd  38414  orcomdd  38488  disjlem14  39222  disjdmqsss  39226  disjdmqscossss  39227  prtlem14  39320  prter2  39327  aev-o  39377  ax12eq  39387  ax12el  39388  ax12indn  39389  ax12indi  39390  lsatn0  39445  lsatcmp  39449  lsatcv0  39477  lfl1dim  39567  lfl1dim2N  39568  lkrss2N  39615  lub0N  39635  glb0N  39639  glbconxN  39824  hl2at  39851  cvrexchlem  39865  cvratlem  39867  cvrat4  39889  psubspi  40193  pointpsubN  40197  elpaddn0  40246  paddasslem17  40282  ispsubcl2N  40393  ldilval  40559  trlord  41015  diaelrnN  41491  cdlemm10N  41564  cdlemn11pre  41656  dihord2pre  41671  dihglblem2N  41740  dihglblem3N  41741  mapdrvallem2  42091  ioin9i8  42646  sn-sup2  42936  incssnn0  43143  fphpd  43244  rmxycomplete  43345  dford3lem1  43454  iocinico  43640  onsupnmax  43656  cantnfresb  43752  cantnf2  43753  tfsconcatb0  43772  tfsconcat0b  43774  sdomne0  43840  sdomne0d  43841  ensucne0OLD  43957  al3im  44074  brtrclfv2  44154  frege129d  44190  frege60a  44305  frege60c  44350  frege70  44360  rfovcnvf1od  44431  clsk1indlem3  44470  neik0pk1imk0  44474  gneispace  44561  gneispaceel2  44571  gneispacess2  44573  dvconstbi  44761  axc5c4c711toc7  44831  axc5c4c711to11  44832  pm14.24  44859  sbiota1  44861  bi33imp12  44918  bi123imp0  44923  ee233  44946  vk15.4j  44955  ssralv2  44958  alrim3con13v  44960  tratrb  44963  onfrALTlem3  44971  onfrALTlem2  44973  19.41rg  44977  hbimpg  44981  hbalg  44982  ax6e2ndeq  44986  e2  45058  ee223  45061  sspwtrALT  45248  sspwtrALT2  45249  suctrALT2  45263  trintALT  45307  isosctrlem1ALT  45360  relpmin  45379  traxext  45404  modelaxreplem2  45406  ssclaxsep  45409  fnchoice  45460  mptfnd  45671  stoweidlem62  46490  2reu8i  47555  2reuimp  47557  ffnafv  47613  lswn0  47898  reupr  47976  reuopreuprim  47980  requad2  48093  bgoldbnnsum3prm  48274  bgoldbtbndlem2  48276  bgoldbtbndlem4  48278  gricsym  48391  gpgedgvtx1  48532  ply1mulgsumlem2  48857  iunord  50145  setrec2fun  50161