Theorem syl6 33

Description: A syllogism rule of inference. The second premise is used to replace the consequent of the first premise. (Contributed by NM, 5-Aug-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 9	. 2 ⊢ (𝜓 → (𝜒 → 𝜃))
4	1, 3	sylcom 28	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  34  syl6com  35  a1dd  48  syl6mpi  64  syl6c  66  com34  83  ex  115  imbitrdi  161  imbitrrdi  162  biimtrdi  163  biimtrrdi  164  pm5.32d  450  con2d  627  con3d  634  expi  641  pm3.37  693  pm5.21ndd  710  pm2.37  810  pm2.81  816  dcim  846  condcOLD  859  con4biddc  862  pm2.54dc  896  pm4.79dc  908  pm2.85dc  910  pm3.12dc  964  dn1dc  966  3jao  1335  xoranor  1419  syl6an  1476  syl10  1477  hbald  1537  ax12  1558  hbimd  1619  nfal  1622  19.21ht  1627  19.30dc  1673  19.23t  1723  hbexd  1740  spimth  1781  spimed  1786  cbv2h  1794  cbv2w  1796  equvini  1804  sbiedh  1833  sbcof2  1856  aev  1858  sb3  1877  hbsb2  1882  sbequilem  1884  sbft  1894  sbi1v  1938  cbvexdh  1973  nf5-1  2075  mo23  2119  moexexdc  2162  euexex  2163  exists2  2175  dvelimdc  2393  rsp2  2580  rgen2a  2584  spcimgft  2879  spcimegft  2881  eueq3dc  2977  moeq3dc  2979  reu6  2992  ssddif  3438  reupick2  3490  ifnebibdc  3648  sssnm  3832  prneimg  3852  dfiun2g  3997  exmidsssnc  4287  exmidundifim  4291  opth1  4322  copsexg  4330  opelopabt  4350  issod  4410  sowlin  4411  suctr  4512  reusv3i  4550  ralxfrALT  4558  ssorduni  4579  onintonm  4609  regexmidlem1  4625  nlimsucg  4658  0elnn  4711  ssrelrn  4914  issref  5111  iotaval  5290  fun11iun  5593  brprcneu  5620  fvssunirng  5642  relfvssunirn  5643  fv3  5650  ndmfvg  5658  ssimaex  5695  fvopab3ig  5708  dff4im  5781  ffnfv  5793  fconstfvm  5857  f1mpt  5895  oprabid  6033  mpoeq123  6063  f1o2ndf1  6374  brtposg  6400  rntpos  6403  dftpos4  6409  smores2  6440  tfri3  6513  rdgss  6529  nntri3or  6639  nndifsnid  6653  nnawordex  6675  eroveu  6773  map0g  6835  fundmen  6959  nneneq  7018  fiintim  7093  snon0  7102  fnfi  7103  infnlbti  7193  exmidonfinlem  7371  exmidontri2or  7428  addclpi  7514  enq0tr  7621  genprndl  7708  genprndu  7709  genpdisj  7710  addlocprlem  7722  nqprloc  7732  recexprlemss1l  7822  recexprlemss1u  7823  suplocexprlemss  7902  elrealeu  8016  ltleletr  8228  negf1o  8528  zletric  9490  zlelttric  9491  zltnle  9492  zmulcl  9500  zdcle  9523  zdclt  9524  zeo  9552  uz11  9745  indstr  9788  eqreznegel  9809  negm  9810  lbzbi  9811  fzdcel  10236  fzm1  10296  qletric  10461  qlelttric  10462  qltnle  10463  qdclt  10465  frecuzrdgtcl  10634  frecuzrdgfunlem  10641  qsqeqor  10872  swrdccatin2d  11276  rennim  11513  maxleast  11724  negfi  11739  fsum3cvg  11889  fproddccvg  12083  prodmodc  12089  ndvdssub  12441  bitsinv1lem  12472  algcvgblem  12571  algcvga  12573  isprm3  12640  oddprmdvds  12877  4sqlem2  12912  imasaddfnlemg  13347  subrngintm  14176  subrgintm  14207  lmodfopnelem1  14288  islssm  14321  lspsneq0  14390  islidlm  14443  epttop  14764  cnptoprest  14913  txcnp  14945  metequiv2  15170  cnlimcim  15345  bj-hbalt  16127  bj-intabssel1  16154  decidin  16161  sumdc2  16163  bj-charfunr  16173  bj-axemptylem  16255  bj-nnen2lp  16317  bj-nnord  16321  setindft  16328  bj-inf2vnlem2  16334  bj-inf2vnlem3  16335  bj-inf2vnlem4  16336  exmidsbthrlem  16390  triap  16397  tridceq  16424