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  202  imbitrdi  250  syl6ib  251  syl6ibr  252  syl6bi  253  syl6bir  254  jaoi  856  pm2.37  970  pm2.81  971  oplem1  1056  3jao  1426  impsingle  1630  al2im  1817  exlimdv  1937  19.23v  1946  19.36imvOLD  1950  spimfw  1970  ax13b  2036  nf5-1  2142  hbald  2169  19.8a  2175  spimedv  2191  19.9d  2197  sbequ1  2241  sbft  2262  cbv2w  2334  spimed  2388  cbv2  2403  cbv2h  2406  ax12  2423  axc11n  2426  equvini  2455  sb2  2479  sb4a  2480  mo3  2559  mopick  2622  moexexlem  2623  dvelimdc  2931  necon1ad  2958  necon4bd  2961  rsp2  3275  mo2icl  3710  2reu1  3891  reuss2  4315  reupick2  4320  elpwunsn  4687  pwpw0  4816  sssn  4829  pwsnOLD  4901  iuneqconst  5008  disjiun  5135  reusv1  5395  reusv3i  5402  ralxfrALT  5413  exneq  5435  opth1  5475  copsexgw  5490  copsexg  5491  opelopabt  5532  solin  5613  wefrc  5670  frinxp  5757  ssrelrn  5893  reuop  6290  ordunidif  6411  oneqmini  6414  suctr  6448  ordsssuc2  6453  iotan0  6531  fv3  6907  ndmfv  6924  ssimaex  6974  fvopab3ig  6992  iinpreima  7068  fvcofneq  7092  dff3  7099  dff4  7100  ffnfv  7115  fnsnr  7160  fprb  7192  elunirn  7247  f1mpt  7257  isomin  7331  oprabidw  7437  oprabid  7438  mpoeq123  7478  sorpsscmpl  7721  dfwe2  7758  ssorduni  7763  ssonprc  7772  nlimsucg  7828  ordunisuc2  7830  tfinds  7846  ssnlim  7872  f1oweALT  7956  el2mpocl  8069  f1o2ndf1  8105  frxp  8109  soxp  8112  poxp2  8126  poxp3  8133  poseq  8141  brtpos  8217  rntpos  8221  dftpos4  8227  onfununi  8338  onnseq  8341  smores2  8351  smo11  8361  tfr3  8396  rdglim2  8429  tz7.48lem  8438  tz7.49  8442  seqomlem2  8448  oawordex  8554  oa00  8556  oaass  8558  om00  8572  odi  8576  omass  8577  oeordi  8584  oelim2  8592  omsmo  8654  eroveu  8803  eceqoveq  8813  map0g  8875  fundmen  9028  sdomdif  9122  onsdominel  9123  pssnn  9165  nneneq  9206  php3  9209  nneneqOLD  9218  php3OLD  9221  onomeneqOLD  9226  pssnnOLD  9262  f1finf1o  9268  f1finf1oOLD  9269  findcard3  9282  findcard3OLD  9283  unblem1  9292  fiint  9321  ixpfi2  9347  dffi2  9415  elfiun  9422  fisup2g  9460  fiinf2g  9492  wemaplem2  9539  preleqALT  9609  inf3lem2  9621  inf3lem3  9622  inf3lem6  9625  noinfep  9652  epfrs  9723  tcmin  9733  r1sdom  9766  tz9.12lem3  9781  rankelb  9816  bndrank  9833  rankunb  9842  rankuni2b  9845  cplem1  9881  karden  9887  carduni  9973  infxpenlem  10005  dfac8alem  10021  alephdom  10073  cardinfima  10089  alephval3  10102  dfac5lem4  10118  dfac5lem5  10119  dfac5  10120  dfac2b  10122  kmlem13  10154  nnadju  10189  ackbij1b  10231  cfub  10241  coflim  10253  cflim2  10255  cfslbn  10259  cfslb2n  10260  cofsmo  10261  cfsmolem  10262  sornom  10269  fincssdom  10315  isf32lem1  10345  isf32lem2  10346  isf32lem9  10353  isf34lem4  10369  isfin1-3  10378  axcc4  10431  domtriomlem  10434  axdc2lem  10440  axdc3lem2  10443  zorn2lem4  10491  zorn2lem6  10493  zornn0g  10497  uniimadom  10536  cardmin  10556  ficard  10557  konigthlem  10560  alephreg  10574  cfpwsdom  10576  axextnd  10583  fpwwe2lem5  10627  fpwwe2lem11  10633  fpwwe2lem12  10634  fpwwe2  10635  canthp1lem2  10645  gchpwdom  10662  winalim2  10688  tskuni  10775  grupr  10789  grur1a  10811  axgroth6  10820  grothomex  10821  eltskm  10835  addclpi  10884  nqereu  10921  ltexnq  10967  nsmallnq  10969  genpn0  10995  genpss  10996  genpnmax  10999  ltaddpr  11026  reclem3pr  11041  reclem4pr  11042  suplem1pr  11044  supsrlem  11103  1re  11211  dedekindle  11375  addrid  11391  negn0  11640  negf1o  11641  negfi  12160  sup2  12167  supadd  12179  supmullem1  12181  supmullem2  12182  zmulcl  12608  zeo  12645  uz11  12844  uzwo  12892  eqreznegel  12915  lbzbi  12917  qextlt  13179  qextle  13180  xrsupsslem  13283  xrinfmsslem  13284  supxrun  13292  supxrpnf  13294  supxrunb1  13295  supxrunb2  13296  fzm1  13578  uzrdgfni  13920  hasheqf1oi  14308  hashreshashfun  14396  leisorel  14418  fundmge2nop0  14450  wrdsymb0  14496  swrdnnn0nd  14603  swrdccatin2d  14691  cshinj  14758  repswcshw  14759  rennim  15183  01sqrexlem6  15191  caubnd  15302  sqreulem  15303  caucvgrlem  15616  fsumcvg  15655  supcvg  15799  prodeq2ii  15854  fprodcvg  15871  prodmo  15877  dvdslelem  16249  bitsinv1lem  16379  bitsshft  16413  smuval2  16420  smupvallem  16421  gcdcllem1  16437  bezoutlem2  16479  bezoutlem3  16480  algcvga  16513  isprm3  16617  isprm5  16641  oddprmdvds  16833  vdwlem13  16923  vdwnnlem1  16925  vdwnnlem3  16927  ramub1lem1  16956  prmgaplem5  16985  imasaddfnlem  17471  divsfval  17490  catpropd  17650  joindmss  18329  meetdmss  18343  psdmrn  18523  odlem1  19398  gexlem1  19442  cygctb  19755  lmodfopnelem1  20501  islss  20538  lspsneq0  20616  lspsneq  20728  psgnodpmr  21135  obselocv  21275  mvrf1  21537  evlseu  21638  mpfrcl  21640  ppttop  22502  epttop  22504  elcls  22569  restntr  22678  cnprest  22785  regsep  22830  nrmsep3  22851  lmmo  22876  cmpsublem  22895  cmpsub  22896  hauscmplem  22902  txcnpi  23104  txcnp  23116  fbun  23336  fbfinnfr  23337  trfbas2  23339  fgcl  23374  filssufilg  23407  ufinffr  23425  isfcls  23505  fclsrest  23520  flimfnfcls  23524  alexsubALTlem2  23544  alexsubALTlem3  23545  alexsubALTlem4  23546  alexsubALT  23547  cnextcn  23563  imasf1oxms  23990  metequiv2  24011  tngngpim  24168  iccpnfcnv  24452  iccpnfhmeo  24453  iscau2  24786  caun0  24790  minveclem3b  24937  itg1climres  25224  mbfi1fseqlem4  25228  ellimc3  25388  limccnp2  25401  dvlip  25502  itgsubstlem  25557  elply2  25702  coefv0  25754  coemulc  25761  ulmss  25901  sineq0  26025  scvxcvx  26480  sqf11  26633  ppiublem1  26695  fsumvma  26706  2sq2  26926  ostth  27132  sltres  27155  nosepdmlem  27176  nocvxminlem  27269  nocvxmin  27270  addsprop  27450  mptelee  28143  brbtwn2  28153  colinearalg  28158  axcontlem4  28215  upgrres1  28560  usgr2trlncl  29007  umgrclwwlkge2  29234  upgr4cycl4dv4e  29428  1to3vfriendship  29524  3cyclfrgrrn1  29528  n4cyclfrgr  29534  frgrncvvdeqlem8  29549  frgrwopreg  29566  2clwwlk2clwwlk  29593  numclwwlk2lem1  29619  frgrreg  29637  frgrogt3nreg  29640  nmcvcn  29936  chlimi  30475  ocsh  30524  shsvs  30564  h1datomi  30822  stcl  31457  stge0  31465  stle1  31466  stm1addi  31486  stm1add3i  31488  cvnsym  31531  mdbr2  31537  dmdbr2  31544  mdsl0  31551  mdsl1i  31562  mdsl2i  31563  cvmdi  31565  atexch  31622  atcvat4i  31638  cdj1i  31674  xrge0iifcnv  32902  esumpr2  33054  sigaclci  33119  cntmeas  33213  mbfmcnt  33256  ballotlemfc0  33480  ballotlemfcc  33481  bnj1379  33830  bnj607  33916  bnj908  33931  bnj938  33937  bnj1174  34003  bnj1280  34020  f1resrcmplf1dlem  34078  fnrelpredd  34081  cusgr3cyclex  34116  loop1cycl  34117  acycgrislfgr  34132  pthacycspth  34137  iccllysconn  34230  satffunlem1lem1  34382  satfvel  34392  sate0fv0  34397  funpsstri  34726  fundmpss  34727  dfon2lem3  34746  dfon2lem4  34747  dfon2lem6  34749  dfon2lem9  34752  dfon2  34753  hbimtg  34767  hbaltg  34768  dfrdg4  34912  btwntriv2  34973  btwncomim  34974  btwnswapid  34978  btwnexch3  34981  ifscgr  35005  lineunray  35108  hilbert1.2  35116  cldbnd  35200  tailfb  35251  meran3  35287  arg-ax  35290  ontopbas  35302  onsuct0  35315  limsucncmpi  35319  ordcmp  35321  onint1  35323  bj-syl66ib  35420  bj-gl4  35462  bj-alexim  35493  bj-nfimt  35504  bj-ax6e  35534  bj-hbalt  35548  axc11n11r  35550  bj-nnfim  35613  bj-nnfan  35615  bj-nnfor  35617  bj-nnford  35618  bj-nnflemaa  35629  bj-nnflemae  35631  bj-19.21t  35636  bj-19.23t  35637  bj-19.42t  35640  bj-sbft  35642  bj-hbsb3t  35655  bj-cbv2hv  35664  bj-equsal1t  35689  bj-0int  35971  bj-bary1lem1  36181  topdifinffinlem  36217  isbasisrelowllem1  36225  isbasisrelowllem2  36226  iooelexlt  36232  finorwe  36252  finxpreclem1  36259  finxpreclem2  36260  isinf2  36275  fvineqsneu  36281  fvineqsneq  36282  pibt2  36287  wl-spae  36379  wl-19.8eqv  36381  wl-nfeqfb  36394  wl-mo3t  36430  wl-ax11-lem3  36438  fin2so  36464  poimirlem29  36506  poimirlem30  36507  poimirlem31  36508  poimirlem32  36509  ismblfin  36518  indexdom  36591  fzmul  36598  heibor1lem  36666  heibor  36678  exidu1  36713  rngoideu  36760  zerdivemp1x  36804  ispridl2  36895  cnf1dd  36947  cnf2dd  36948  cnfn1dd  36949  cnfn2dd  36950  orcomdd  37024  disjlem14  37657  disjdmqsss  37661  disjdmqscossss  37662  prtlem14  37733  prter2  37740  aev-o  37790  ax12eq  37800  ax12el  37801  ax12indn  37802  ax12indi  37803  lsatn0  37858  lsatcmp  37862  lsatcv0  37890  lfl1dim  37980  lfl1dim2N  37981  lkrss2N  38028  lub0N  38048  glb0N  38052  glbconxN  38238  hl2at  38265  cvrexchlem  38279  cvratlem  38281  cvrat4  38303  psubspi  38607  pointpsubN  38611  elpaddn0  38660  paddasslem17  38696  ispsubcl2N  38807  ldilval  38973  trlord  39429  diaelrnN  39905  cdlemm10N  39978  cdlemn11pre  40070  dihord2pre  40085  dihglblem2N  40154  dihglblem3N  40155  mapdrvallem2  40505  ioin9i8  41020  sn-sup2  41339  incssnn0  41435  fphpd  41540  rmxycomplete  41642  dford3lem1  41751  iocinico  41947  onsupnmax  41963  cantnfresb  42060  cantnf2  42061  tfsconcatb0  42080  tfsconcat0b  42082  sdomne0  42150  sdomne0d  42151  ensucne0OLD  42267  al3im  42384  brtrclfv2  42464  frege129d  42500  frege60a  42615  frege60c  42660  frege70  42670  rfovcnvf1od  42741  clsk1indlem3  42780  neik0pk1imk0  42784  gneispace  42871  gneispaceel2  42881  gneispacess2  42883  dvconstbi  43079  axc5c4c711toc7  43149  axc5c4c711to11  43150  pm14.24  43177  sbiota1  43179  bi33imp12  43237  bi123imp0  43243  ee233  43266  vk15.4j  43275  ssralv2  43278  alrim3con13v  43280  tratrb  43283  onfrALTlem3  43291  onfrALTlem2  43293  19.41rg  43297  hbimpg  43301  hbalg  43302  ax6e2ndeq  43306  e2  43378  ee223  43381  sspwtrALT  43569  sspwtrALT2  43570  suctrALT2  43584  trintALT  43628  isosctrlem1ALT  43681  fnchoice  43699  mptfnd  43931  stoweidlem62  44765  2reu8i  45808  2reuimp  45810  ffnafv  45866  lswn0  46099  reupr  46177  reuopreuprim  46181  requad2  46278  bgoldbnnsum3prm  46459  bgoldbtbndlem2  46461  bgoldbtbndlem4  46463  ply1mulgsumlem2  47022  iunord  47675  setrec2fun  47691