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  629  con3d  636  expi  643  pm3.37  696  pm5.21ndd  713  pm2.37  813  pm2.81  819  dcim  849  condcOLD  862  con4biddc  865  pm2.54dc  899  pm4.79dc  911  pm2.85dc  913  pm3.12dc  967  dn1dc  969  3jao  1338  xoranor  1422  syl6an  1479  syl10  1480  hbald  1540  ax12  1561  hbimd  1622  nfal  1625  19.21ht  1630  19.30dc  1676  19.23t  1725  hbexd  1742  spimth  1784  spimed  1789  cbv2h  1797  cbv2w  1799  equvini  1807  sbiedh  1836  sbcof2  1859  aev  1861  sb3  1880  hbsb2  1885  sbequilem  1887  sbft  1897  sbi1v  1941  cbvexdh  1976  nf5-1  2078  mo23  2122  moexexdc  2165  euexex  2166  exists2  2178  dvelimdc  2405  rsp2  2592  rgen2a  2596  spcimgft  2892  spcimegft  2894  eueq3dc  2990  moeq3dc  2992  reu6  3005  ssddif  3454  reupick2  3506  ifnebibdc  3667  sssnm  3857  prneimg  3877  dfiun2g  4022  exmidsssnc  4315  exmidundifim  4319  opth1  4351  copsexg  4359  opelopabt  4379  issod  4439  sowlin  4440  suctr  4541  reusv3i  4579  ralxfrALT  4587  ssorduni  4608  onintonm  4638  regexmidlem1  4654  nlimsucg  4687  0elnn  4740  ssrelrn  4946  issref  5144  iotaval  5323  fun11iun  5634  brprcneu  5662  fvssunirng  5684  relfvssunirn  5685  fv3  5692  ndmfvg  5700  ssimaex  5737  fvopab3ig  5750  dff4im  5822  ffnfv  5834  fconstfvm  5901  f1mpt  5943  oprabid  6081  mpoeq123  6111  f1o2ndf1  6423  brtposg  6484  rntpos  6487  dftpos4  6493  smores2  6524  tfri3  6597  rdgss  6613  nntri3or  6725  nndifsnid  6739  nnawordex  6761  eroveu  6859  map0g  6921  fundmen  7046  nneneq  7110  fiintim  7190  snon0  7201  fnfi  7202  infnlbti  7316  exmidonfinlem  7495  exmidontri2or  7552  addclpi  7638  enq0tr  7745  genprndl  7832  genprndu  7833  genpdisj  7834  addlocprlem  7846  nqprloc  7856  recexprlemss1l  7946  recexprlemss1u  7947  suplocexprlemss  8026  elrealeu  8140  ltleletr  8351  negf1o  8651  zletric  9617  zlelttric  9618  zltnle  9619  zmulcl  9627  zdcle  9650  zdclt  9651  zeo  9679  uz11  9873  indstr  9921  eqreznegel  9942  negm  9943  lbzbi  9944  fzdcel  10370  fzm1  10430  qletric  10597  qlelttric  10598  qltnle  10599  qdclt  10601  frecuzrdgtcl  10770  frecuzrdgfunlem  10777  qsqeqor  11008  swrdccatin2d  11429  rennim  11680  maxleast  11891  negfi  11906  fsum3cvg  12057  fproddccvg  12251  prodmodc  12257  ndvdssub  12609  bitsinv1lem  12640  algcvgblem  12739  algcvga  12741  isprm3  12808  oddprmdvds  13045  4sqlem2  13080  imasaddfnlemg  13516  subrngintm  14346  subrgintm  14377  lmodfopnelem1  14459  islssm  14492  lspsneq0  14561  islidlm  14614  epttop  14942  cnptoprest  15091  txcnp  15123  metequiv2  15348  cnlimcim  15523  umgrclwwlkge2  16384  bj-hbalt  16522  bj-intabssel1  16549  decidin  16556  sumdc2  16558  bj-charfunr  16567  bj-axemptylem  16649  bj-nnen2lp  16711  bj-nnord  16715  setindft  16722  bj-inf2vnlem2  16728  bj-inf2vnlem3  16729  bj-inf2vnlem4  16730  exmidsbthrlem  16789  triap  16800  tridceq  16828