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  2836  spcimegft  2838  eueq3dc  2934  moeq3dc  2936  reu6  2949  ssddif  3393  reupick2  3445  ifnebibdc  3600  sssnm  3780  prneimg  3800  dfiun2g  3944  exmidsssnc  4232  exmidundifim  4236  opth1  4265  copsexg  4273  opelopabt  4292  issod  4350  sowlin  4351  suctr  4452  reusv3i  4490  ralxfrALT  4498  ssorduni  4519  onintonm  4549  regexmidlem1  4565  nlimsucg  4598  0elnn  4651  issref  5048  iotaval  5226  fun11iun  5521  brprcneu  5547  fvssunirng  5569  relfvssunirn  5570  fv3  5577  ndmfvg  5585  ssimaex  5618  fvopab3ig  5631  dff4im  5704  ffnfv  5716  fconstfvm  5776  f1mpt  5814  oprabid  5950  mpoeq123  5977  f1o2ndf1  6281  brtposg  6307  rntpos  6310  dftpos4  6316  smores2  6347  tfri3  6420  rdgss  6436  nntri3or  6546  nndifsnid  6560  nnawordex  6582  eroveu  6680  map0g  6742  fundmen  6860  nneneq  6913  fiintim  6985  snon0  6994  fnfi  6995  infnlbti  7085  exmidonfinlem  7253  exmidontri2or  7303  addclpi  7387  enq0tr  7494  genprndl  7581  genprndu  7582  genpdisj  7583  addlocprlem  7595  nqprloc  7605  recexprlemss1l  7695  recexprlemss1u  7696  suplocexprlemss  7775  elrealeu  7889  ltleletr  8101  negf1o  8401  zletric  9361  zlelttric  9362  zltnle  9363  zmulcl  9370  zdcle  9393  zdclt  9394  zeo  9422  uz11  9615  indstr  9658  eqreznegel  9679  negm  9680  lbzbi  9681  fzdcel  10106  fzm1  10166  qletric  10311  qlelttric  10312  qltnle  10313  qdclt  10315  frecuzrdgtcl  10483  frecuzrdgfunlem  10490  qsqeqor  10721  rennim  11146  maxleast  11357  negfi  11371  fsum3cvg  11521  fproddccvg  11715  prodmodc  11721  ndvdssub  12071  algcvgblem  12187  algcvga  12189  isprm3  12256  oddprmdvds  12492  4sqlem2  12527  imasaddfnlemg  12897  subrngintm  13708  subrgintm  13739  lmodfopnelem1  13820  islssm  13853  lspsneq0  13922  islidlm  13975  epttop  14258  cnptoprest  14407  txcnp  14439  metequiv2  14664  cnlimcim  14825  bj-hbalt  15255  bj-intabssel1  15282  decidin  15289  sumdc2  15291  bj-charfunr  15302  bj-axemptylem  15384  bj-nnen2lp  15446  bj-nnord  15450  setindft  15457  bj-inf2vnlem2  15463  bj-inf2vnlem3  15464  bj-inf2vnlem4  15465  exmidsbthrlem  15512  triap  15519  tridceq  15546