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  1942  cbvexdh  1978  nf5-1  2080  mo23  2124  moexexdc  2167  euexex  2168  exists2  2180  dvelimdc  2407  rsp2  2594  rgen2a  2598  spcimgft  2895  spcimegft  2897  eueq3dc  2993  moeq3dc  2995  reu6  3008  ssddif  3457  reupick2  3509  ifnebibdc  3670  sssnm  3860  prneimg  3880  dfiun2g  4025  exmidsssnc  4318  exmidundifim  4322  opth1  4354  copsexg  4362  opelopabt  4382  issod  4442  sowlin  4443  suctr  4544  reusv3i  4582  ralxfrALT  4590  ssorduni  4611  onintonm  4641  regexmidlem1  4657  nlimsucg  4690  0elnn  4743  ssrelrn  4949  issref  5147  iotaval  5326  fun11iun  5637  brprcneu  5665  fvssunirng  5687  relfvssunirn  5688  fv3  5695  ndmfvg  5703  ssimaex  5740  fvopab3ig  5753  dff4im  5825  ffnfv  5837  fconstfvm  5904  f1mpt  5946  oprabid  6084  mpoeq123  6114  f1o2ndf1  6426  brtposg  6487  rntpos  6490  dftpos4  6496  smores2  6527  tfri3  6600  rdgss  6616  nntri3or  6728  nndifsnid  6742  nnawordex  6764  eroveu  6862  map0g  6924  fundmen  7049  nneneq  7113  fiintim  7193  snon0  7204  fnfi  7205  infnlbti  7319  exmidonfinlem  7498  exmidontri2or  7555  addclpi  7647  enq0tr  7754  genprndl  7841  genprndu  7842  genpdisj  7843  addlocprlem  7855  nqprloc  7865  recexprlemss1l  7955  recexprlemss1u  7956  suplocexprlemss  8035  elrealeu  8149  ltleletr  8360  negf1o  8660  zletric  9626  zlelttric  9627  zltnle  9628  zmulcl  9636  zdcle  9659  zdclt  9660  zeo  9689  uz11  9883  indstr  9931  eqreznegel  9952  negm  9953  lbzbi  9954  fzdcel  10380  fzm1  10441  qletric  10608  qlelttric  10609  qltnle  10610  qdclt  10612  frecuzrdgtcl  10781  frecuzrdgfunlem  10788  qsqeqor  11019  swrdccatin2d  11444  rennim  11695  maxleast  11906  negfi  11921  fsum3cvg  12072  fproddccvg  12266  prodmodc  12272  ndvdssub  12624  bitsinv1lem  12655  algcvgblem  12754  algcvga  12756  isprm3  12823  oddprmdvds  13060  4sqlem2  13095  ballotfilemfc0  13157  ballotfilemfcc  13158  imasaddfnlemg  13548  subrngintm  14380  subrgintm  14411  lmodfopnelem1  14521  islssm  14554  lspsneq0  14623  islidlm  14676  epttop  15004  cnptoprest  15153  txcnp  15185  metequiv2  15410  cnlimcim  15585  umgrclwwlkge2  16446  bj-hbalt  16584  bj-intabssel1  16611  decidin  16618  sumdc2  16620  bj-charfunr  16629  bj-axemptylem  16711  bj-nnen2lp  16773  bj-nnord  16777  setindft  16784  bj-inf2vnlem2  16790  bj-inf2vnlem3  16791  bj-inf2vnlem4  16792  exmidsbthrlem  16851  triap  16862  tridceq  16890