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  1424  impsingle  1623  al2im  1810  exlimdv  1930  19.23v  1939  spimfw  1962  ax13b  2028  nf5-1  2142  hbald  2165  19.8a  2178  spimedv  2194  19.9d  2200  sbequ1  2245  sbft  2267  cbv2w  2337  spimed  2390  cbv2  2405  cbv2h  2408  ax12  2425  axc11n  2428  equvini  2457  sb2  2481  sb4a  2482  mo3  2561  mopick  2622  moexexlem  2623  dvelimdc  2927  necon1ad  2954  necon4bd  2957  rsp2  3274  mo2icl  3722  2reu1  3905  reuss2  4331  reupick2  4336  elpwunsn  4688  pwpw0  4817  sssn  4830  iuneqconst  5007  disjiun  5135  reusv1  5402  reusv3i  5409  ralxfrALT  5420  exneq  5445  opth1  5485  copsexgw  5500  copsexg  5501  opelopabt  5541  solin  5622  wefrc  5682  frinxp  5770  ssrelrn  5907  dmcosseq  5989  reuop  6314  ordunidif  6434  oneqmini  6437  suctr  6471  ordsssuc2  6476  iotan0  6552  fv3  6924  ndmfv  6941  ssimaex  6993  fvopab3ig  7011  iinpreima  7088  fvcofneq  7112  dff3  7119  dff4  7120  ffnfv  7138  fnsnr  7184  fprb  7213  elunirn  7270  f1mpt  7280  isomin  7356  oprabidw  7461  oprabid  7462  mpoeq123  7504  sorpsscmpl  7752  dfwe2  7792  ssorduni  7797  ssonprc  7806  nlimsucg  7862  ordunisuc2  7864  tfinds  7880  ssnlim  7906  f1oweALT  7995  mptcnfimad  8009  el2mpocl  8109  f1o2ndf1  8145  frxp  8149  soxp  8152  poxp2  8166  poxp3  8173  poseq  8181  brtpos  8258  rntpos  8262  dftpos4  8268  onfununi  8379  onnseq  8382  smores2  8392  smo11  8402  tfr3  8437  rdglim2  8470  tz7.48lem  8479  tz7.49  8483  seqomlem2  8489  oawordex  8593  oa00  8595  oaass  8597  om00  8611  odi  8615  omass  8616  oeordi  8623  oelim2  8631  omsmo  8694  eroveu  8850  eceqoveq  8860  map0g  8922  fundmen  9069  sdomdif  9163  onsdominel  9164  pssnn  9206  nneneq  9243  php3  9246  nneneqOLD  9255  php3OLD  9258  onomeneqOLD  9263  f1finf1o  9302  f1finf1oOLD  9303  findcard3  9315  findcard3OLD  9316  unblem1  9325  fiint  9363  fiintOLD  9364  ixpfi2  9387  dffi2  9460  elfiun  9467  fisup2g  9505  fiinf2g  9537  wemaplem2  9584  preleqALT  9654  inf3lem2  9666  inf3lem3  9667  inf3lem6  9670  noinfep  9697  epfrs  9768  tcmin  9778  r1sdom  9811  tz9.12lem3  9826  rankelb  9861  bndrank  9878  rankunb  9887  rankuni2b  9890  cplem1  9926  karden  9932  carduni  10018  infxpenlem  10050  dfac8alem  10066  alephdom  10118  cardinfima  10134  alephval3  10147  dfac5lem4  10163  dfac5lem5  10164  dfac5lem4OLD  10165  dfac5  10166  dfac2b  10168  kmlem13  10200  nnadju  10235  ackbij1b  10275  cfub  10286  coflim  10298  cflim2  10300  cfslbn  10304  cfslb2n  10305  cofsmo  10306  cfsmolem  10307  sornom  10314  fincssdom  10360  isf32lem1  10390  isf32lem2  10391  isf32lem9  10398  isf34lem4  10414  isfin1-3  10423  axcc4  10476  domtriomlem  10479  axdc2lem  10485  axdc3lem2  10488  zorn2lem4  10536  zorn2lem6  10538  zornn0g  10542  uniimadom  10581  cardmin  10601  ficard  10602  konigthlem  10605  alephreg  10619  cfpwsdom  10621  axextnd  10628  fpwwe2lem5  10672  fpwwe2lem11  10678  fpwwe2lem12  10679  fpwwe2  10680  canthp1lem2  10690  gchpwdom  10707  winalim2  10733  tskuni  10820  grupr  10834  grur1a  10856  axgroth6  10865  grothomex  10866  eltskm  10880  addclpi  10929  nqereu  10966  ltexnq  11012  nsmallnq  11014  genpn0  11040  genpss  11041  genpnmax  11044  ltaddpr  11071  reclem3pr  11086  reclem4pr  11087  suplem1pr  11089  supsrlem  11148  1re  11258  dedekindle  11422  addrid  11438  negn0  11689  negf1o  11690  negfi  12214  sup2  12221  supadd  12233  supmullem1  12235  supmullem2  12236  zmulcl  12663  zeo  12701  uz11  12900  uzwo  12950  eqreznegel  12973  lbzbi  12975  qextlt  13241  qextle  13242  xrsupsslem  13345  xrinfmsslem  13346  supxrun  13354  supxrpnf  13356  supxrunb1  13357  supxrunb2  13358  fzm1  13643  uzrdgfni  13995  hasheqf1oi  14386  hashreshashfun  14474  leisorel  14495  fundmge2nop0  14537  wrdsymb0  14583  swrdnnn0nd  14690  swrdccatin2d  14778  cshinj  14845  repswcshw  14846  rennim  15274  01sqrexlem6  15282  caubnd  15393  sqreulem  15394  caucvgrlem  15705  fsumcvg  15744  supcvg  15888  prodeq2ii  15943  fprodcvg  15962  prodmo  15968  dvdslelem  16342  bitsinv1lem  16474  bitsshft  16508  smuval2  16515  smupvallem  16516  gcdcllem1  16532  bezoutlem2  16573  bezoutlem3  16574  algcvga  16612  isprm3  16716  isprm5  16740  oddprmdvds  16936  vdwlem13  17026  vdwnnlem1  17028  vdwnnlem3  17030  ramub1lem1  17059  prmgaplem5  17088  imasaddfnlem  17574  divsfval  17593  catpropd  17753  joindmss  18436  meetdmss  18450  psdmrn  18630  odlem1  19567  gexlem1  19611  cygctb  19924  rngisomring1  20484  lmodfopnelem1  20912  islss  20949  lspsneq0  21027  lspsneq  21141  psgnodpmr  21625  obselocv  21765  mvrf1  22023  evlseu  22124  mpfrcl  22126  ppttop  23029  epttop  23031  elcls  23096  restntr  23205  cnprest  23312  regsep  23357  nrmsep3  23378  lmmo  23403  cmpsublem  23422  cmpsub  23423  hauscmplem  23429  txcnpi  23631  txcnp  23643  fbun  23863  fbfinnfr  23864  trfbas2  23866  fgcl  23901  filssufilg  23934  ufinffr  23952  isfcls  24032  fclsrest  24047  flimfnfcls  24051  alexsubALTlem2  24071  alexsubALTlem3  24072  alexsubALTlem4  24073  alexsubALT  24074  cnextcn  24090  imasf1oxms  24517  metequiv2  24538  tngngpim  24695  iccpnfcnv  24988  iccpnfhmeo  24989  iscau2  25324  caun0  25328  minveclem3b  25475  itg1climres  25763  mbfi1fseqlem4  25767  ellimc3  25928  limccnp2  25941  dvlip  26046  itgsubstlem  26103  elply2  26249  coefv0  26301  coemulc  26308  ulmss  26454  sineq0  26580  scvxcvx  27043  sqf11  27196  ppiublem1  27260  fsumvma  27271  2sq2  27491  ostth  27697  sltres  27721  nosepdmlem  27742  nocvxminlem  27836  nocvxmin  27837  addsprop  28023  mptelee  28924  brbtwn2  28934  colinearalg  28939  axcontlem4  28996  upgrres1  29344  usgr2trlncl  29792  umgrclwwlkge2  30019  upgr4cycl4dv4e  30213  1to3vfriendship  30309  3cyclfrgrrn1  30313  n4cyclfrgr  30319  frgrncvvdeqlem8  30334  frgrwopreg  30351  2clwwlk2clwwlk  30378  numclwwlk2lem1  30404  frgrreg  30422  frgrogt3nreg  30425  nmcvcn  30723  chlimi  31262  ocsh  31311  shsvs  31351  h1datomi  31609  stcl  32244  stge0  32252  stle1  32253  stm1addi  32273  stm1add3i  32275  cvnsym  32318  mdbr2  32324  dmdbr2  32331  mdsl0  32338  mdsl1i  32349  mdsl2i  32350  cvmdi  32352  atexch  32409  atcvat4i  32425  cdj1i  32461  1arithufdlem4  33554  xrge0iifcnv  33893  esumpr2  34047  sigaclci  34112  cntmeas  34206  mbfmcnt  34249  ballotlemfc0  34473  ballotlemfcc  34474  bnj1379  34822  bnj607  34908  bnj908  34923  bnj938  34929  bnj1174  34995  bnj1280  35012  f1resrcmplf1dlem  35078  fnrelpredd  35081  axnulg  35084  cusgr3cyclex  35120  loop1cycl  35121  acycgrislfgr  35136  pthacycspth  35141  iccllysconn  35234  satffunlem1lem1  35386  satfvel  35396  sate0fv0  35401  funpsstri  35746  fundmpss  35747  dfon2lem3  35766  dfon2lem4  35767  dfon2lem6  35769  dfon2lem9  35772  dfon2  35773  hbimtg  35787  hbaltg  35788  dfrdg4  35932  btwntriv2  35993  btwncomim  35994  btwnswapid  35998  btwnexch3  36001  ifscgr  36025  lineunray  36128  hilbert1.2  36136  cldbnd  36308  tailfb  36359  meran3  36395  arg-ax  36398  ontopbas  36410  onsuct0  36423  limsucncmpi  36427  ordcmp  36429  onint1  36431  weiunpo  36447  bj-syl66ib  36537  bj-gl4  36577  bj-alexim  36609  bj-nfimt  36620  bj-ax6e  36650  bj-hbalt  36663  axc11n11r  36665  bj-nnfim  36728  bj-nnfan  36730  bj-nnfor  36732  bj-nnford  36733  bj-nnflemaa  36744  bj-nnflemae  36746  bj-19.21t  36751  bj-19.23t  36752  bj-19.42t  36755  bj-sbft  36757  bj-hbsb3t  36770  bj-cbv2hv  36779  bj-equsal1t  36804  bj-0int  37083  bj-bary1lem1  37293  topdifinffinlem  37329  isbasisrelowllem1  37337  isbasisrelowllem2  37338  iooelexlt  37344  finorwe  37364  finxpreclem1  37371  finxpreclem2  37372  isinf2  37387  fvineqsneu  37393  fvineqsneq  37394  pibt2  37399  wl-spae  37501  wl-19.8eqv  37503  wl-nfeqfb  37516  wl-mo3t  37556  wl-ax11-lem3  37567  fin2so  37593  poimirlem29  37635  poimirlem30  37636  poimirlem31  37637  poimirlem32  37638  ismblfin  37647  indexdom  37720  fzmul  37727  heibor1lem  37795  heibor  37807  exidu1  37842  rngoideu  37889  zerdivemp1x  37933  ispridl2  38024  cnf1dd  38076  cnf2dd  38077  cnfn1dd  38078  cnfn2dd  38079  orcomdd  38153  disjlem14  38779  disjdmqsss  38783  disjdmqscossss  38784  prtlem14  38855  prter2  38862  aev-o  38912  ax12eq  38922  ax12el  38923  ax12indn  38924  ax12indi  38925  lsatn0  38980  lsatcmp  38984  lsatcv0  39012  lfl1dim  39102  lfl1dim2N  39103  lkrss2N  39150  lub0N  39170  glb0N  39174  glbconxN  39360  hl2at  39387  cvrexchlem  39401  cvratlem  39403  cvrat4  39425  psubspi  39729  pointpsubN  39733  elpaddn0  39782  paddasslem17  39818  ispsubcl2N  39929  ldilval  40095  trlord  40551  diaelrnN  41027  cdlemm10N  41100  cdlemn11pre  41192  dihord2pre  41207  dihglblem2N  41276  dihglblem3N  41277  mapdrvallem2  41627  ioin9i8  42225  sn-sup2  42477  incssnn0  42698  fphpd  42803  rmxycomplete  42905  dford3lem1  43014  iocinico  43200  onsupnmax  43216  cantnfresb  43313  cantnf2  43314  tfsconcatb0  43333  tfsconcat0b  43335  sdomne0  43402  sdomne0d  43403  ensucne0OLD  43519  al3im  43636  brtrclfv2  43716  frege129d  43752  frege60a  43867  frege60c  43912  frege70  43922  rfovcnvf1od  43993  clsk1indlem3  44032  neik0pk1imk0  44036  gneispace  44123  gneispaceel2  44133  gneispacess2  44135  dvconstbi  44329  axc5c4c711toc7  44399  axc5c4c711to11  44400  pm14.24  44427  sbiota1  44429  bi33imp12  44487  bi123imp0  44493  ee233  44516  vk15.4j  44525  ssralv2  44528  alrim3con13v  44530  tratrb  44533  onfrALTlem3  44541  onfrALTlem2  44543  19.41rg  44547  hbimpg  44551  hbalg  44552  ax6e2ndeq  44556  e2  44628  ee223  44631  sspwtrALT  44819  sspwtrALT2  44820  suctrALT2  44834  trintALT  44878  isosctrlem1ALT  44931  traxext  44937  modelaxreplem2  44943  ssclaxsep  44946  fnchoice  44966  mptfnd  45185  stoweidlem62  46017  2reu8i  47062  2reuimp  47064  ffnafv  47120  lswn0  47368  reupr  47446  reuopreuprim  47450  requad2  47547  bgoldbnnsum3prm  47728  bgoldbtbndlem2  47730  bgoldbtbndlem4  47732  gricsym  47827  gpgedgvtx1  47954  ply1mulgsumlem2  48232  iunord  48906  setrec2fun  48922