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  2150  hbald  2173  19.8a  2186  spimedv  2202  19.9d  2208  sbequ1  2253  sbft  2274  cbv2w  2339  spimed  2390  cbv2  2405  cbv2h  2408  ax12  2425  axc11n  2428  equvini  2457  sb2  2481  sb4a  2482  mo3  2561  mopick  2622  moexexlem  2623  dvelimdc  2921  necon1ad  2947  necon4bd  2950  rsp2  3251  mo2icl  3670  2reu1  3845  reuss2  4277  reupick2  4282  elpwunsn  4638  pwpw0  4766  sssn  4779  iuneqconst  4955  disjiun  5083  reusv1  5339  reusv3i  5346  ralxfrALT  5357  exneq  5382  opth1  5420  copsexgw  5435  copsexg  5436  opelopabt  5477  solin  5556  wefrc  5615  frinxp  5704  ssrelrn  5841  dmcosseq  5924  dmcosseqOLD  5925  reuop  6248  ordunidif  6364  oneqmini  6367  suctr  6402  ordsssuc2  6407  iotan0  6479  fv3  6849  ndmfv  6863  ssimaex  6916  fvopab3ig  6934  iinpreima  7011  fvcofneq  7035  dff3  7042  dff4  7043  ffnfv  7061  fnsnr  7106  fprb  7137  elunirn  7194  f1mpt  7204  isomin  7280  oprabidw  7386  oprabid  7387  mpoeq123  7427  sorpsscmpl  7676  dfwe2  7716  ssorduni  7721  ssonprc  7729  nlimsucg  7781  ordunisuc2  7783  tfinds  7799  ssnlim  7825  f1oweALT  7913  mptcnfimad  7927  el2mpocl  8025  f1o2ndf1  8061  frxp  8065  soxp  8068  poxp2  8082  poxp3  8089  poseq  8097  brtpos  8174  rntpos  8178  dftpos4  8184  onfununi  8270  onnseq  8273  smores2  8283  smo11  8293  tfr3  8327  rdglim2  8360  tz7.48lem  8369  tz7.49  8373  seqomlem2  8379  oawordex  8481  oa00  8483  oaass  8485  om00  8499  odi  8503  omass  8504  oeordi  8511  oelim2  8519  omsmo  8582  eroveu  8745  eceqoveq  8755  map0g  8817  fundmen  8963  sdomdif  9048  onsdominel  9049  pssnn  9088  nneneq  9125  php3  9128  f1finf1o  9167  findcard3  9177  unblem1  9186  fiint  9221  ixpfi2  9244  dffi2  9317  elfiun  9324  fisup2g  9363  fiinf2g  9396  wemaplem2  9443  elirrv  9493  preleqALT  9517  inf3lem2  9529  inf3lem3  9530  inf3lem6  9533  noinfep  9560  epfrs  9631  tcmin  9639  r1sdom  9677  tz9.12lem3  9692  rankelb  9727  bndrank  9744  rankunb  9753  rankuni2b  9756  cplem1  9792  karden  9798  carduni  9884  infxpenlem  9914  dfac8alem  9930  alephdom  9982  cardinfima  9998  alephval3  10011  dfac5lem4  10027  dfac5lem5  10028  dfac5lem4OLD  10029  dfac5  10030  dfac2b  10032  kmlem13  10064  nnadju  10099  ackbij1b  10139  cfub  10150  coflim  10162  cflim2  10164  cfslbn  10168  cfslb2n  10169  cofsmo  10170  cfsmolem  10171  sornom  10178  fincssdom  10224  isf32lem1  10254  isf32lem2  10255  isf32lem9  10262  isf34lem4  10278  isfin1-3  10287  axcc4  10340  domtriomlem  10343  axdc2lem  10349  axdc3lem2  10352  zorn2lem4  10400  zorn2lem6  10402  zornn0g  10406  uniimadom  10445  cardmin  10465  ficard  10466  konigthlem  10469  alephreg  10483  cfpwsdom  10485  axextnd  10492  fpwwe2lem5  10536  fpwwe2lem11  10542  fpwwe2lem12  10543  fpwwe2  10544  canthp1lem2  10554  gchpwdom  10571  winalim2  10597  tskuni  10684  grupr  10698  grur1a  10720  axgroth6  10729  grothomex  10730  eltskm  10744  addclpi  10793  nqereu  10830  ltexnq  10876  nsmallnq  10878  genpn0  10904  genpss  10905  genpnmax  10908  ltaddpr  10935  reclem3pr  10950  reclem4pr  10951  suplem1pr  10953  supsrlem  11012  1re  11122  dedekindle  11287  addrid  11303  negn0  11556  negf1o  11557  negfi  12081  sup2  12088  supadd  12100  supmullem1  12102  supmullem2  12103  zmulcl  12531  zeo  12569  uz11  12767  uzwo  12819  eqreznegel  12842  lbzbi  12844  qextlt  13112  qextle  13113  xrsupsslem  13216  xrinfmsslem  13217  supxrun  13225  supxrpnf  13227  supxrunb1  13228  supxrunb2  13229  fzm1  13517  uzrdgfni  13875  hasheqf1oi  14268  hashreshashfun  14356  leisorel  14377  fundmge2nop0  14419  wrdsymb0  14466  swrdnnn0nd  14574  swrdccatin2d  14661  cshinj  14728  repswcshw  14729  rennim  15156  01sqrexlem6  15164  caubnd  15276  sqreulem  15277  caucvgrlem  15590  fsumcvg  15629  supcvg  15773  prodeq2ii  15828  fprodcvg  15847  prodmo  15853  dvdslelem  16230  bitsinv1lem  16362  bitsshft  16396  smuval2  16403  smupvallem  16404  gcdcllem1  16420  bezoutlem2  16461  bezoutlem3  16462  algcvga  16500  isprm3  16604  isprm5  16628  oddprmdvds  16825  vdwlem13  16915  vdwnnlem1  16917  vdwnnlem3  16919  ramub1lem1  16948  prmgaplem5  16977  imasaddfnlem  17442  divsfval  17461  catpropd  17625  joindmss  18293  meetdmss  18307  psdmrn  18489  odlem1  19457  gexlem1  19501  cygctb  19814  rngisomring1  20396  lmodfopnelem1  20841  islss  20877  lspsneq0  20955  lspsneq  21069  psgnodpmr  21537  obselocv  21675  mvrf1  21933  evlseu  22028  mpfrcl  22030  ppttop  22932  epttop  22934  elcls  22998  restntr  23107  cnprest  23214  regsep  23259  nrmsep3  23280  lmmo  23305  cmpsublem  23324  cmpsub  23325  hauscmplem  23331  txcnpi  23533  txcnp  23545  fbun  23765  fbfinnfr  23766  trfbas2  23768  fgcl  23803  filssufilg  23836  ufinffr  23854  isfcls  23934  fclsrest  23949  flimfnfcls  23953  alexsubALTlem2  23973  alexsubALTlem3  23974  alexsubALTlem4  23975  alexsubALT  23976  cnextcn  23992  imasf1oxms  24414  metequiv2  24435  tngngpim  24584  iccpnfcnv  24879  iccpnfhmeo  24880  iscau2  25214  caun0  25218  minveclem3b  25365  itg1climres  25652  mbfi1fseqlem4  25656  ellimc3  25817  limccnp2  25830  dvlip  25935  itgsubstlem  25992  elply2  26138  coefv0  26190  coemulc  26197  ulmss  26343  sineq0  26470  scvxcvx  26933  sqf11  27086  ppiublem1  27150  fsumvma  27161  2sq2  27381  ostth  27587  sltres  27611  nosepdmlem  27632  nobdaymin  27726  nocvxminlem  27727  addsprop  27929  mpteleeOLD  28884  brbtwn2  28894  colinearalg  28899  axcontlem4  28956  upgrres1  29302  usgr2trlncl  29749  umgrclwwlkge2  29982  upgr4cycl4dv4e  30176  1to3vfriendship  30272  3cyclfrgrrn1  30276  n4cyclfrgr  30282  frgrncvvdeqlem8  30297  frgrwopreg  30314  2clwwlk2clwwlk  30341  numclwwlk2lem1  30367  frgrreg  30385  frgrogt3nreg  30388  nmcvcn  30686  chlimi  31225  ocsh  31274  shsvs  31314  h1datomi  31572  stcl  32207  stge0  32215  stle1  32216  stm1addi  32236  stm1add3i  32238  cvnsym  32281  mdbr2  32287  dmdbr2  32294  mdsl0  32301  mdsl1i  32312  mdsl2i  32313  cvmdi  32315  atexch  32372  atcvat4i  32388  cdj1i  32424  1arithufdlem4  33523  xrge0iifcnv  33957  esumpr2  34091  sigaclci  34156  cntmeas  34250  mbfmcnt  34292  ballotlemfc0  34517  ballotlemfcc  34518  bnj1379  34853  bnj607  34939  bnj908  34954  bnj938  34960  bnj1174  35026  bnj1280  35043  f1resrcmplf1dlem  35109  fnrelpredd  35113  r1filimi  35125  axnulg  35130  tz9.1regs  35141  cusgr3cyclex  35191  loop1cycl  35192  acycgrislfgr  35207  pthacycspth  35212  iccllysconn  35305  satffunlem1lem1  35457  satfvel  35467  sate0fv0  35472  antnestlaw2  35747  funpsstri  35821  fundmpss  35822  dfon2lem3  35838  dfon2lem4  35839  dfon2lem6  35841  dfon2lem9  35844  dfon2  35845  hbimtg  35859  hbaltg  35860  dfrdg4  36006  btwntriv2  36067  btwncomim  36068  btwnswapid  36072  btwnexch3  36075  ifscgr  36099  lineunray  36202  hilbert1.2  36210  cldbnd  36381  tailfb  36432  meran3  36468  arg-ax  36471  ontopbas  36483  onsuct0  36496  limsucncmpi  36500  ordcmp  36502  onint1  36504  weiunpo  36520  bj-syl66ib  36610  bj-gl4  36650  bj-alexim  36682  bj-nfimt  36693  bj-ax6e  36723  bj-hbalt  36736  axc11n11r  36738  bj-nnfim  36801  bj-nnfan  36803  bj-nnfor  36805  bj-nnford  36806  bj-nnflemaa  36817  bj-nnflemae  36819  bj-19.21t  36824  bj-19.23t  36825  bj-19.42t  36828  bj-sbft  36830  bj-hbsb3t  36843  bj-cbv2hv  36852  bj-equsal1t  36877  bj-0int  37156  bj-bary1lem1  37366  topdifinffinlem  37402  isbasisrelowllem1  37410  isbasisrelowllem2  37411  iooelexlt  37417  finorwe  37437  finxpreclem1  37444  finxpreclem2  37445  isinf2  37460  fvineqsneu  37466  fvineqsneq  37467  pibt2  37472  wl-spae  37576  wl-19.8eqv  37578  wl-nfeqfb  37591  wl-mo3t  37631  fin2so  37657  poimirlem29  37699  poimirlem30  37700  poimirlem31  37701  poimirlem32  37702  ismblfin  37711  indexdom  37784  fzmul  37791  heibor1lem  37859  heibor  37871  exidu1  37906  rngoideu  37953  zerdivemp1x  37997  ispridl2  38088  cnf1dd  38140  cnf2dd  38141  cnfn1dd  38142  cnfn2dd  38143  orcomdd  38217  disjlem14  38906  disjdmqsss  38910  disjdmqscossss  38911  prtlem14  38983  prter2  38990  aev-o  39040  ax12eq  39050  ax12el  39051  ax12indn  39052  ax12indi  39053  lsatn0  39108  lsatcmp  39112  lsatcv0  39140  lfl1dim  39230  lfl1dim2N  39231  lkrss2N  39278  lub0N  39298  glb0N  39302  glbconxN  39487  hl2at  39514  cvrexchlem  39528  cvratlem  39530  cvrat4  39552  psubspi  39856  pointpsubN  39860  elpaddn0  39909  paddasslem17  39945  ispsubcl2N  40056  ldilval  40222  trlord  40678  diaelrnN  41154  cdlemm10N  41227  cdlemn11pre  41319  dihord2pre  41334  dihglblem2N  41403  dihglblem3N  41404  mapdrvallem2  41754  ioin9i8  42310  sn-sup2  42599  incssnn0  42818  fphpd  42923  rmxycomplete  43024  dford3lem1  43133  iocinico  43319  onsupnmax  43335  cantnfresb  43431  cantnf2  43432  tfsconcatb0  43451  tfsconcat0b  43453  sdomne0  43520  sdomne0d  43521  ensucne0OLD  43637  al3im  43754  brtrclfv2  43834  frege129d  43870  frege60a  43985  frege60c  44030  frege70  44040  rfovcnvf1od  44111  clsk1indlem3  44150  neik0pk1imk0  44154  gneispace  44241  gneispaceel2  44251  gneispacess2  44253  dvconstbi  44441  axc5c4c711toc7  44511  axc5c4c711to11  44512  pm14.24  44539  sbiota1  44541  bi33imp12  44598  bi123imp0  44603  ee233  44626  vk15.4j  44635  ssralv2  44638  alrim3con13v  44640  tratrb  44643  onfrALTlem3  44651  onfrALTlem2  44653  19.41rg  44657  hbimpg  44661  hbalg  44662  ax6e2ndeq  44666  e2  44738  ee223  44741  sspwtrALT  44928  sspwtrALT2  44929  suctrALT2  44943  trintALT  44987  isosctrlem1ALT  45040  relpmin  45059  traxext  45084  modelaxreplem2  45086  ssclaxsep  45089  fnchoice  45140  mptfnd  45353  stoweidlem62  46174  2reu8i  47227  2reuimp  47229  ffnafv  47285  lswn0  47558  reupr  47636  reuopreuprim  47640  requad2  47737  bgoldbnnsum3prm  47918  bgoldbtbndlem2  47920  bgoldbtbndlem4  47922  gricsym  48035  gpgedgvtx1  48176  ply1mulgsumlem2  48502  iunord  49791  setrec2fun  49807