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  3254  mo2icl  3673  2reu1  3848  reuss2  4279  reupick2  4284  elpwunsn  4642  pwpw0  4770  sssn  4783  iuneqconst  4959  disjiun  5087  reusv1  5343  reusv3i  5350  ralxfrALT  5361  exneq  5386  opth1  5424  copsexgw  5439  copsexg  5440  opelopabt  5481  solin  5560  wefrc  5619  frinxp  5708  ssrelrn  5844  dmcosseq  5928  dmcosseqOLD  5929  reuop  6252  ordunidif  6368  oneqmini  6371  suctr  6406  ordsssuc2  6411  iotan0  6483  fv3  6853  ndmfv  6867  ssimaex  6920  fvopab3ig  6938  iinpreima  7016  fvcofneq  7040  dff3  7047  dff4  7048  ffnfv  7066  fnsnr  7111  fprb  7142  elunirn  7199  f1mpt  7209  isomin  7285  oprabidw  7391  oprabid  7392  mpoeq123  7432  sorpsscmpl  7681  dfwe2  7721  ssorduni  7726  ssonprc  7734  nlimsucg  7786  ordunisuc2  7788  tfinds  7804  ssnlim  7830  f1oweALT  7918  mptcnfimad  7932  el2mpocl  8030  f1o2ndf1  8066  frxp  8070  soxp  8073  poxp2  8087  poxp3  8094  poseq  8102  brtpos  8179  rntpos  8183  dftpos4  8189  onfununi  8275  onnseq  8278  smores2  8288  smo11  8298  tfr3  8332  rdglim2  8365  tz7.48lem  8374  tz7.49  8378  seqomlem2  8384  oawordex  8486  oa00  8488  oaass  8490  om00  8504  odi  8508  omass  8509  oeordi  8517  oelim2  8525  omsmo  8588  eroveu  8753  eceqoveq  8763  map0g  8826  fundmen  8972  sdomdif  9057  onsdominel  9058  pssnn  9097  nneneq  9134  php3  9137  f1finf1o  9177  findcard3  9187  unblem1  9196  fiint  9231  ixpfi2  9254  dffi2  9330  elfiun  9337  fisup2g  9376  fiinf2g  9409  wemaplem2  9456  elirrv  9506  preleqALT  9530  inf3lem2  9542  inf3lem3  9543  inf3lem6  9546  noinfep  9573  epfrs  9644  tcmin  9652  r1sdom  9690  tz9.12lem3  9705  rankelb  9740  bndrank  9757  rankunb  9766  rankuni2b  9769  cplem1  9805  karden  9811  carduni  9897  infxpenlem  9927  dfac8alem  9943  alephdom  9995  cardinfima  10011  alephval3  10024  dfac5lem4  10040  dfac5lem5  10041  dfac5lem4OLD  10042  dfac5  10043  dfac2b  10045  kmlem13  10077  nnadju  10112  ackbij1b  10152  cfub  10163  coflim  10175  cflim2  10177  cfslbn  10181  cfslb2n  10182  cofsmo  10183  cfsmolem  10184  sornom  10191  fincssdom  10237  isf32lem1  10267  isf32lem2  10268  isf32lem9  10275  isf34lem4  10291  isfin1-3  10300  axcc4  10353  domtriomlem  10356  axdc2lem  10362  axdc3lem2  10365  zorn2lem4  10413  zorn2lem6  10415  zornn0g  10419  uniimadom  10458  cardmin  10478  ficard  10479  konigthlem  10483  alephreg  10497  cfpwsdom  10499  axextnd  10506  fpwwe2lem5  10550  fpwwe2lem11  10556  fpwwe2lem12  10557  fpwwe2  10558  canthp1lem2  10568  gchpwdom  10585  winalim2  10611  tskuni  10698  grupr  10712  grur1a  10734  axgroth6  10743  grothomex  10744  eltskm  10758  addclpi  10807  nqereu  10844  ltexnq  10890  nsmallnq  10892  genpn0  10918  genpss  10919  genpnmax  10922  ltaddpr  10949  reclem3pr  10964  reclem4pr  10965  suplem1pr  10967  supsrlem  11026  1re  11136  dedekindle  11301  addrid  11317  negn0  11570  negf1o  11571  negfi  12095  sup2  12102  supadd  12114  supmullem1  12116  supmullem2  12117  zmulcl  12544  zeo  12582  uz11  12780  uzwo  12828  eqreznegel  12851  lbzbi  12853  qextlt  13122  qextle  13123  xrsupsslem  13226  xrinfmsslem  13227  supxrun  13235  supxrpnf  13237  supxrunb1  13238  supxrunb2  13239  fzm1  13527  uzrdgfni  13885  hasheqf1oi  14278  hashreshashfun  14366  leisorel  14387  fundmge2nop0  14429  wrdsymb0  14476  swrdnnn0nd  14584  swrdccatin2d  14671  cshinj  14738  repswcshw  14739  rennim  15166  01sqrexlem6  15174  caubnd  15286  sqreulem  15287  caucvgrlem  15600  fsumcvg  15639  supcvg  15783  prodeq2ii  15838  fprodcvg  15857  prodmo  15863  dvdslelem  16240  bitsinv1lem  16372  bitsshft  16406  smuval2  16413  smupvallem  16414  gcdcllem1  16430  bezoutlem2  16471  bezoutlem3  16472  algcvga  16510  isprm3  16614  isprm5  16638  oddprmdvds  16835  vdwlem13  16925  vdwnnlem1  16927  vdwnnlem3  16929  ramub1lem1  16958  prmgaplem5  16987  imasaddfnlem  17453  divsfval  17472  catpropd  17636  joindmss  18304  meetdmss  18318  psdmrn  18500  odlem1  19468  gexlem1  19512  cygctb  19825  rngisomring1  20408  lmodfopnelem1  20853  islss  20889  lspsneq0  20967  lspsneq  21081  psgnodpmr  21549  obselocv  21687  mvrf1  21945  evlseu  22042  mpfrcl  22044  ppttop  22955  epttop  22957  elcls  23021  restntr  23130  cnprest  23237  regsep  23282  nrmsep3  23303  lmmo  23328  cmpsublem  23347  cmpsub  23348  hauscmplem  23354  txcnpi  23556  txcnp  23568  fbun  23788  fbfinnfr  23789  trfbas2  23791  fgcl  23826  filssufilg  23859  ufinffr  23877  isfcls  23957  fclsrest  23972  flimfnfcls  23976  alexsubALTlem2  23996  alexsubALTlem3  23997  alexsubALTlem4  23998  alexsubALT  23999  cnextcn  24015  imasf1oxms  24437  metequiv2  24458  tngngpim  24607  iccpnfcnv  24902  iccpnfhmeo  24903  iscau2  25237  caun0  25241  minveclem3b  25388  itg1climres  25675  mbfi1fseqlem4  25679  ellimc3  25840  limccnp2  25853  dvlip  25958  itgsubstlem  26015  elply2  26161  coefv0  26213  coemulc  26220  ulmss  26366  sineq0  26493  scvxcvx  26956  sqf11  27109  ppiublem1  27173  fsumvma  27184  2sq2  27404  ostth  27610  sltres  27634  nosepdmlem  27655  nobdaymin  27753  nocvxminlem  27754  addsprop  27958  mpteleeOLD  28951  brbtwn2  28961  colinearalg  28966  axcontlem4  29023  upgrres1  29369  usgr2trlncl  29816  umgrclwwlkge2  30049  upgr4cycl4dv4e  30243  1to3vfriendship  30339  3cyclfrgrrn1  30343  n4cyclfrgr  30349  frgrncvvdeqlem8  30364  frgrwopreg  30381  2clwwlk2clwwlk  30408  numclwwlk2lem1  30434  frgrreg  30452  frgrogt3nreg  30455  nmcvcn  30753  chlimi  31292  ocsh  31341  shsvs  31381  h1datomi  31639  stcl  32274  stge0  32282  stle1  32283  stm1addi  32303  stm1add3i  32305  cvnsym  32348  mdbr2  32354  dmdbr2  32361  mdsl0  32368  mdsl1i  32379  mdsl2i  32380  cvmdi  32382  atexch  32439  atcvat4i  32455  cdj1i  32491  1arithufdlem4  33609  xrge0iifcnv  34071  esumpr2  34205  sigaclci  34270  cntmeas  34364  mbfmcnt  34406  ballotlemfc0  34631  ballotlemfcc  34632  bnj1379  34967  bnj607  35053  bnj908  35068  bnj938  35074  bnj1174  35140  bnj1280  35157  f1resrcmplf1dlem  35223  fnrelpredd  35228  r1filimi  35240  axnulg  35245  fineqvinfep  35262  tz9.1regs  35271  cusgr3cyclex  35311  loop1cycl  35312  acycgrislfgr  35327  pthacycspth  35332  iccllysconn  35425  satffunlem1lem1  35577  satfvel  35587  sate0fv0  35592  antnestlaw2  35867  funpsstri  35941  fundmpss  35942  dfon2lem3  35958  dfon2lem4  35959  dfon2lem6  35961  dfon2lem9  35964  dfon2  35965  hbimtg  35979  hbaltg  35980  dfrdg4  36126  btwntriv2  36187  btwncomim  36188  btwnswapid  36192  btwnexch3  36195  ifscgr  36219  lineunray  36322  hilbert1.2  36330  cldbnd  36501  tailfb  36552  meran3  36588  arg-ax  36591  ontopbas  36603  onsuct0  36616  limsucncmpi  36620  ordcmp  36622  onint1  36624  weiunpo  36640  bj-syl66ib  36730  bj-gl4  36770  bj-alexim  36802  bj-nfimt  36813  bj-ax6e  36844  bj-hbalt  36857  axc11n11r  36859  bj-nnfim  36922  bj-nnfan  36924  bj-nnfor  36926  bj-nnford  36927  bj-nnflemaa  36938  bj-nnflemae  36940  bj-19.21t  36945  bj-19.23t  36946  bj-19.42t  36949  bj-sbft  36951  bj-hbsb3t  36964  bj-cbv2hv  36973  bj-equsal1t  36998  bj-0int  37277  bj-bary1lem1  37487  topdifinffinlem  37523  isbasisrelowllem1  37531  isbasisrelowllem2  37532  iooelexlt  37538  finorwe  37558  finxpreclem1  37565  finxpreclem2  37566  isinf2  37581  fvineqsneu  37587  fvineqsneq  37588  pibt2  37593  wl-spae  37697  wl-19.8eqv  37699  wl-nfeqfb  37712  wl-mo3t  37752  wl-eujustlem1  37764  fin2so  37779  poimirlem29  37821  poimirlem30  37822  poimirlem31  37823  poimirlem32  37824  ismblfin  37833  indexdom  37906  fzmul  37913  heibor1lem  37981  heibor  37993  exidu1  38028  rngoideu  38075  zerdivemp1x  38119  ispridl2  38210  cnf1dd  38262  cnf2dd  38263  cnfn1dd  38264  cnfn2dd  38265  orcomdd  38339  disjlem14  39073  disjdmqsss  39077  disjdmqscossss  39078  prtlem14  39171  prter2  39178  aev-o  39228  ax12eq  39238  ax12el  39239  ax12indn  39240  ax12indi  39241  lsatn0  39296  lsatcmp  39300  lsatcv0  39328  lfl1dim  39418  lfl1dim2N  39419  lkrss2N  39466  lub0N  39486  glb0N  39490  glbconxN  39675  hl2at  39702  cvrexchlem  39716  cvratlem  39718  cvrat4  39740  psubspi  40044  pointpsubN  40048  elpaddn0  40097  paddasslem17  40133  ispsubcl2N  40244  ldilval  40410  trlord  40866  diaelrnN  41342  cdlemm10N  41415  cdlemn11pre  41507  dihord2pre  41522  dihglblem2N  41591  dihglblem3N  41592  mapdrvallem2  41942  ioin9i8  42498  sn-sup2  42782  incssnn0  42989  fphpd  43094  rmxycomplete  43195  dford3lem1  43304  iocinico  43490  onsupnmax  43506  cantnfresb  43602  cantnf2  43603  tfsconcatb0  43622  tfsconcat0b  43624  sdomne0  43690  sdomne0d  43691  ensucne0OLD  43807  al3im  43924  brtrclfv2  44004  frege129d  44040  frege60a  44155  frege60c  44200  frege70  44210  rfovcnvf1od  44281  clsk1indlem3  44320  neik0pk1imk0  44324  gneispace  44411  gneispaceel2  44421  gneispacess2  44423  dvconstbi  44611  axc5c4c711toc7  44681  axc5c4c711to11  44682  pm14.24  44709  sbiota1  44711  bi33imp12  44768  bi123imp0  44773  ee233  44796  vk15.4j  44805  ssralv2  44808  alrim3con13v  44810  tratrb  44813  onfrALTlem3  44821  onfrALTlem2  44823  19.41rg  44827  hbimpg  44831  hbalg  44832  ax6e2ndeq  44836  e2  44908  ee223  44911  sspwtrALT  45098  sspwtrALT2  45099  suctrALT2  45113  trintALT  45157  isosctrlem1ALT  45210  relpmin  45229  traxext  45254  modelaxreplem2  45256  ssclaxsep  45259  fnchoice  45310  mptfnd  45522  stoweidlem62  46342  2reu8i  47395  2reuimp  47397  ffnafv  47453  lswn0  47726  reupr  47804  reuopreuprim  47808  requad2  47905  bgoldbnnsum3prm  48086  bgoldbtbndlem2  48088  bgoldbtbndlem4  48090  gricsym  48203  gpgedgvtx1  48344  ply1mulgsumlem2  48669  iunord  49957  setrec2fun  49973