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  625  con3d  632  expi  639  pm3.37  690  pm5.21ndd  706  pm2.37  806  pm2.81  812  dcim  842  condcOLD  855  con4biddc  858  pm2.54dc  892  pm4.79dc  904  pm2.85dc  906  pm3.12dc  960  dn1dc  962  3jao  1312  xoranor  1388  syl6an  1445  syl10  1446  hbald  1502  ax12  1523  hbimd  1584  nfal  1587  19.21ht  1592  19.30dc  1638  19.23t  1688  hbexd  1705  spimth  1746  spimed  1751  cbv2h  1759  cbv2w  1761  equvini  1769  sbiedh  1798  sbcof2  1821  aev  1823  sb3  1842  hbsb2  1847  sbequilem  1849  sbft  1859  sbi1v  1903  cbvexdh  1938  nf5-1  2040  mo23  2083  moexexdc  2126  euexex  2127  exists2  2139  dvelimdc  2357  rsp2  2544  rgen2a  2548  spcimgft  2837  spcimegft  2839  eueq3dc  2935  moeq3dc  2937  reu6  2950  ssddif  3394  reupick2  3446  ifnebibdc  3601  sssnm  3781  prneimg  3801  dfiun2g  3945  exmidsssnc  4233  exmidundifim  4237  opth1  4266  copsexg  4274  opelopabt  4293  issod  4351  sowlin  4352  suctr  4453  reusv3i  4491  ralxfrALT  4499  ssorduni  4520  onintonm  4550  regexmidlem1  4566  nlimsucg  4599  0elnn  4652  issref  5049  iotaval  5227  fun11iun  5522  brprcneu  5548  fvssunirng  5570  relfvssunirn  5571  fv3  5578  ndmfvg  5586  ssimaex  5619  fvopab3ig  5632  dff4im  5705  ffnfv  5717  fconstfvm  5777  f1mpt  5815  oprabid  5951  mpoeq123  5978  f1o2ndf1  6283  brtposg  6309  rntpos  6312  dftpos4  6318  smores2  6349  tfri3  6422  rdgss  6438  nntri3or  6548  nndifsnid  6562  nnawordex  6584  eroveu  6682  map0g  6744  fundmen  6862  nneneq  6915  fiintim  6987  snon0  6996  fnfi  6997  infnlbti  7087  exmidonfinlem  7255  exmidontri2or  7305  addclpi  7389  enq0tr  7496  genprndl  7583  genprndu  7584  genpdisj  7585  addlocprlem  7597  nqprloc  7607  recexprlemss1l  7697  recexprlemss1u  7698  suplocexprlemss  7777  elrealeu  7891  ltleletr  8103  negf1o  8403  zletric  9364  zlelttric  9365  zltnle  9366  zmulcl  9373  zdcle  9396  zdclt  9397  zeo  9425  uz11  9618  indstr  9661  eqreznegel  9682  negm  9683  lbzbi  9684  fzdcel  10109  fzm1  10169  qletric  10314  qlelttric  10315  qltnle  10316  qdclt  10318  frecuzrdgtcl  10486  frecuzrdgfunlem  10493  qsqeqor  10724  rennim  11149  maxleast  11360  negfi  11374  fsum3cvg  11524  fproddccvg  11718  prodmodc  11724  ndvdssub  12074  algcvgblem  12190  algcvga  12192  isprm3  12259  oddprmdvds  12495  4sqlem2  12530  imasaddfnlemg  12900  subrngintm  13711  subrgintm  13742  lmodfopnelem1  13823  islssm  13856  lspsneq0  13925  islidlm  13978  epttop  14269  cnptoprest  14418  txcnp  14450  metequiv2  14675  cnlimcim  14850  bj-hbalt  15325  bj-intabssel1  15352  decidin  15359  sumdc2  15361  bj-charfunr  15372  bj-axemptylem  15454  bj-nnen2lp  15516  bj-nnord  15520  setindft  15527  bj-inf2vnlem2  15533  bj-inf2vnlem3  15534  bj-inf2vnlem4  15535  exmidsbthrlem  15582  triap  15589  tridceq  15616