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  856  pm2.37  971  pm2.81  972  oplem1  1057  3jao  1425  impsingle  1625  al2im  1812  exlimdv  1932  19.23v  1941  19.36imvOLD  1945  spimfw  1965  ax13b  2031  nf5-1  2145  hbald  2169  19.8a  2182  spimedv  2198  19.9d  2204  sbequ1  2249  sbft  2271  cbv2w  2343  spimed  2396  cbv2  2411  cbv2h  2414  ax12  2431  axc11n  2434  equvini  2463  sb2  2487  sb4a  2488  mo3  2567  mopick  2628  moexexlem  2629  dvelimdc  2936  necon1ad  2963  necon4bd  2966  rsp2  3283  mo2icl  3736  2reu1  3919  reuss2  4345  reupick2  4350  elpwunsn  4707  pwpw0  4838  sssn  4851  iuneqconst  5026  disjiun  5154  reusv1  5415  reusv3i  5422  ralxfrALT  5433  exneq  5455  opth1  5495  copsexgw  5510  copsexg  5511  opelopabt  5551  solin  5634  wefrc  5694  frinxp  5782  ssrelrn  5919  dmcosseq  5999  reuop  6324  ordunidif  6444  oneqmini  6447  suctr  6481  ordsssuc2  6486  iotan0  6563  fv3  6938  ndmfv  6955  ssimaex  7007  fvopab3ig  7025  iinpreima  7102  fvcofneq  7127  dff3  7134  dff4  7135  ffnfv  7153  fnsnr  7199  fprb  7231  elunirn  7288  f1mpt  7298  isomin  7373  oprabidw  7479  oprabid  7480  mpoeq123  7522  sorpsscmpl  7769  dfwe2  7809  ssorduni  7814  ssonprc  7823  nlimsucg  7879  ordunisuc2  7881  tfinds  7897  ssnlim  7923  f1oweALT  8013  mptcnfimad  8027  el2mpocl  8127  f1o2ndf1  8163  frxp  8167  soxp  8170  poxp2  8184  poxp3  8191  poseq  8199  brtpos  8276  rntpos  8280  dftpos4  8286  onfununi  8397  onnseq  8400  smores2  8410  smo11  8420  tfr3  8455  rdglim2  8488  tz7.48lem  8497  tz7.49  8501  seqomlem2  8507  oawordex  8613  oa00  8615  oaass  8617  om00  8631  odi  8635  omass  8636  oeordi  8643  oelim2  8651  omsmo  8714  eroveu  8870  eceqoveq  8880  map0g  8942  fundmen  9096  sdomdif  9191  onsdominel  9192  pssnn  9234  nneneq  9272  php3  9275  nneneqOLD  9284  php3OLD  9287  onomeneqOLD  9292  f1finf1o  9333  f1finf1oOLD  9334  findcard3  9346  findcard3OLD  9347  unblem1  9356  fiint  9394  fiintOLD  9395  ixpfi2  9420  dffi2  9492  elfiun  9499  fisup2g  9537  fiinf2g  9569  wemaplem2  9616  preleqALT  9686  inf3lem2  9698  inf3lem3  9699  inf3lem6  9702  noinfep  9729  epfrs  9800  tcmin  9810  r1sdom  9843  tz9.12lem3  9858  rankelb  9893  bndrank  9910  rankunb  9919  rankuni2b  9922  cplem1  9958  karden  9964  carduni  10050  infxpenlem  10082  dfac8alem  10098  alephdom  10150  cardinfima  10166  alephval3  10179  dfac5lem4  10195  dfac5lem5  10196  dfac5lem4OLD  10197  dfac5  10198  dfac2b  10200  kmlem13  10232  nnadju  10267  ackbij1b  10307  cfub  10318  coflim  10330  cflim2  10332  cfslbn  10336  cfslb2n  10337  cofsmo  10338  cfsmolem  10339  sornom  10346  fincssdom  10392  isf32lem1  10422  isf32lem2  10423  isf32lem9  10430  isf34lem4  10446  isfin1-3  10455  axcc4  10508  domtriomlem  10511  axdc2lem  10517  axdc3lem2  10520  zorn2lem4  10568  zorn2lem6  10570  zornn0g  10574  uniimadom  10613  cardmin  10633  ficard  10634  konigthlem  10637  alephreg  10651  cfpwsdom  10653  axextnd  10660  fpwwe2lem5  10704  fpwwe2lem11  10710  fpwwe2lem12  10711  fpwwe2  10712  canthp1lem2  10722  gchpwdom  10739  winalim2  10765  tskuni  10852  grupr  10866  grur1a  10888  axgroth6  10897  grothomex  10898  eltskm  10912  addclpi  10961  nqereu  10998  ltexnq  11044  nsmallnq  11046  genpn0  11072  genpss  11073  genpnmax  11076  ltaddpr  11103  reclem3pr  11118  reclem4pr  11119  suplem1pr  11121  supsrlem  11180  1re  11290  dedekindle  11454  addrid  11470  negn0  11719  negf1o  11720  negfi  12244  sup2  12251  supadd  12263  supmullem1  12265  supmullem2  12266  zmulcl  12692  zeo  12729  uz11  12928  uzwo  12976  eqreznegel  12999  lbzbi  13001  qextlt  13265  qextle  13266  xrsupsslem  13369  xrinfmsslem  13370  supxrun  13378  supxrpnf  13380  supxrunb1  13381  supxrunb2  13382  fzm1  13664  uzrdgfni  14009  hasheqf1oi  14400  hashreshashfun  14488  leisorel  14509  fundmge2nop0  14551  wrdsymb0  14597  swrdnnn0nd  14704  swrdccatin2d  14792  cshinj  14859  repswcshw  14860  rennim  15288  01sqrexlem6  15296  caubnd  15407  sqreulem  15408  caucvgrlem  15721  fsumcvg  15760  supcvg  15904  prodeq2ii  15959  fprodcvg  15978  prodmo  15984  dvdslelem  16357  bitsinv1lem  16487  bitsshft  16521  smuval2  16528  smupvallem  16529  gcdcllem1  16545  bezoutlem2  16587  bezoutlem3  16588  algcvga  16626  isprm3  16730  isprm5  16754  oddprmdvds  16950  vdwlem13  17040  vdwnnlem1  17042  vdwnnlem3  17044  ramub1lem1  17073  prmgaplem5  17102  imasaddfnlem  17588  divsfval  17607  catpropd  17767  joindmss  18449  meetdmss  18463  psdmrn  18643  odlem1  19577  gexlem1  19621  cygctb  19934  rngisomring1  20494  lmodfopnelem1  20918  islss  20955  lspsneq0  21033  lspsneq  21147  psgnodpmr  21631  obselocv  21771  mvrf1  22029  evlseu  22130  mpfrcl  22132  ppttop  23035  epttop  23037  elcls  23102  restntr  23211  cnprest  23318  regsep  23363  nrmsep3  23384  lmmo  23409  cmpsublem  23428  cmpsub  23429  hauscmplem  23435  txcnpi  23637  txcnp  23649  fbun  23869  fbfinnfr  23870  trfbas2  23872  fgcl  23907  filssufilg  23940  ufinffr  23958  isfcls  24038  fclsrest  24053  flimfnfcls  24057  alexsubALTlem2  24077  alexsubALTlem3  24078  alexsubALTlem4  24079  alexsubALT  24080  cnextcn  24096  imasf1oxms  24523  metequiv2  24544  tngngpim  24701  iccpnfcnv  24994  iccpnfhmeo  24995  iscau2  25330  caun0  25334  minveclem3b  25481  itg1climres  25769  mbfi1fseqlem4  25773  ellimc3  25934  limccnp2  25947  dvlip  26052  itgsubstlem  26109  elply2  26255  coefv0  26307  coemulc  26314  ulmss  26458  sineq0  26584  scvxcvx  27047  sqf11  27200  ppiublem1  27264  fsumvma  27275  2sq2  27495  ostth  27701  sltres  27725  nosepdmlem  27746  nocvxminlem  27840  nocvxmin  27841  addsprop  28027  mptelee  28928  brbtwn2  28938  colinearalg  28943  axcontlem4  29000  upgrres1  29348  usgr2trlncl  29796  umgrclwwlkge2  30023  upgr4cycl4dv4e  30217  1to3vfriendship  30313  3cyclfrgrrn1  30317  n4cyclfrgr  30323  frgrncvvdeqlem8  30338  frgrwopreg  30355  2clwwlk2clwwlk  30382  numclwwlk2lem1  30408  frgrreg  30426  frgrogt3nreg  30429  nmcvcn  30727  chlimi  31266  ocsh  31315  shsvs  31355  h1datomi  31613  stcl  32248  stge0  32256  stle1  32257  stm1addi  32277  stm1add3i  32279  cvnsym  32322  mdbr2  32328  dmdbr2  32335  mdsl0  32342  mdsl1i  32353  mdsl2i  32354  cvmdi  32356  atexch  32413  atcvat4i  32429  cdj1i  32465  1arithufdlem4  33540  xrge0iifcnv  33879  esumpr2  34031  sigaclci  34096  cntmeas  34190  mbfmcnt  34233  ballotlemfc0  34457  ballotlemfcc  34458  bnj1379  34806  bnj607  34892  bnj908  34907  bnj938  34913  bnj1174  34979  bnj1280  34996  f1resrcmplf1dlem  35062  fnrelpredd  35065  axnulg  35068  cusgr3cyclex  35104  loop1cycl  35105  acycgrislfgr  35120  pthacycspth  35125  iccllysconn  35218  satffunlem1lem1  35370  satfvel  35380  sate0fv0  35385  funpsstri  35729  fundmpss  35730  dfon2lem3  35749  dfon2lem4  35750  dfon2lem6  35752  dfon2lem9  35755  dfon2  35756  hbimtg  35770  hbaltg  35771  dfrdg4  35915  btwntriv2  35976  btwncomim  35977  btwnswapid  35981  btwnexch3  35984  ifscgr  36008  lineunray  36111  hilbert1.2  36119  cldbnd  36292  tailfb  36343  meran3  36379  arg-ax  36382  ontopbas  36394  onsuct0  36407  limsucncmpi  36411  ordcmp  36413  onint1  36415  weiunpo  36431  bj-syl66ib  36521  bj-gl4  36561  bj-alexim  36593  bj-nfimt  36604  bj-ax6e  36634  bj-hbalt  36647  axc11n11r  36649  bj-nnfim  36712  bj-nnfan  36714  bj-nnfor  36716  bj-nnford  36717  bj-nnflemaa  36728  bj-nnflemae  36730  bj-19.21t  36735  bj-19.23t  36736  bj-19.42t  36739  bj-sbft  36741  bj-hbsb3t  36754  bj-cbv2hv  36763  bj-equsal1t  36788  bj-0int  37067  bj-bary1lem1  37277  topdifinffinlem  37313  isbasisrelowllem1  37321  isbasisrelowllem2  37322  iooelexlt  37328  finorwe  37348  finxpreclem1  37355  finxpreclem2  37356  isinf2  37371  fvineqsneu  37377  fvineqsneq  37378  pibt2  37383  wl-spae  37475  wl-19.8eqv  37477  wl-nfeqfb  37490  wl-mo3t  37530  wl-ax11-lem3  37541  fin2so  37567  poimirlem29  37609  poimirlem30  37610  poimirlem31  37611  poimirlem32  37612  ismblfin  37621  indexdom  37694  fzmul  37701  heibor1lem  37769  heibor  37781  exidu1  37816  rngoideu  37863  zerdivemp1x  37907  ispridl2  37998  cnf1dd  38050  cnf2dd  38051  cnfn1dd  38052  cnfn2dd  38053  orcomdd  38127  disjlem14  38754  disjdmqsss  38758  disjdmqscossss  38759  prtlem14  38830  prter2  38837  aev-o  38887  ax12eq  38897  ax12el  38898  ax12indn  38899  ax12indi  38900  lsatn0  38955  lsatcmp  38959  lsatcv0  38987  lfl1dim  39077  lfl1dim2N  39078  lkrss2N  39125  lub0N  39145  glb0N  39149  glbconxN  39335  hl2at  39362  cvrexchlem  39376  cvratlem  39378  cvrat4  39400  psubspi  39704  pointpsubN  39708  elpaddn0  39757  paddasslem17  39793  ispsubcl2N  39904  ldilval  40070  trlord  40526  diaelrnN  41002  cdlemm10N  41075  cdlemn11pre  41167  dihord2pre  41182  dihglblem2N  41251  dihglblem3N  41252  mapdrvallem2  41602  ioin9i8  42201  sn-sup2  42447  incssnn0  42667  fphpd  42772  rmxycomplete  42874  dford3lem1  42983  iocinico  43173  onsupnmax  43189  cantnfresb  43286  cantnf2  43287  tfsconcatb0  43306  tfsconcat0b  43308  sdomne0  43375  sdomne0d  43376  ensucne0OLD  43492  al3im  43609  brtrclfv2  43689  frege129d  43725  frege60a  43840  frege60c  43885  frege70  43895  rfovcnvf1od  43966  clsk1indlem3  44005  neik0pk1imk0  44009  gneispace  44096  gneispaceel2  44106  gneispacess2  44108  dvconstbi  44303  axc5c4c711toc7  44373  axc5c4c711to11  44374  pm14.24  44401  sbiota1  44403  bi33imp12  44461  bi123imp0  44467  ee233  44490  vk15.4j  44499  ssralv2  44502  alrim3con13v  44504  tratrb  44507  onfrALTlem3  44515  onfrALTlem2  44517  19.41rg  44521  hbimpg  44525  hbalg  44526  ax6e2ndeq  44530  e2  44602  ee223  44605  sspwtrALT  44793  sspwtrALT2  44794  suctrALT2  44808  trintALT  44852  isosctrlem1ALT  44905  traxext  44910  fnchoice  44929  mptfnd  45150  stoweidlem62  45983  2reu8i  47028  2reuimp  47030  ffnafv  47086  lswn0  47318  reupr  47396  reuopreuprim  47400  requad2  47497  bgoldbnnsum3prm  47678  bgoldbtbndlem2  47680  bgoldbtbndlem4  47682  gricsym  47774  ply1mulgsumlem2  48116  iunord  48768  setrec2fun  48784