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  1505  ax12  1526  hbimd  1587  nfal  1590  19.21ht  1595  19.30dc  1641  19.23t  1691  hbexd  1708  spimth  1749  spimed  1754  cbv2h  1762  cbv2w  1764  equvini  1772  sbiedh  1801  sbcof2  1824  aev  1826  sb3  1845  hbsb2  1850  sbequilem  1852  sbft  1862  sbi1v  1906  cbvexdh  1941  nf5-1  2043  mo23  2086  moexexdc  2129  euexex  2130  exists2  2142  dvelimdc  2360  rsp2  2547  rgen2a  2551  spcimgft  2840  spcimegft  2842  eueq3dc  2938  moeq3dc  2940  reu6  2953  ssddif  3398  reupick2  3450  ifnebibdc  3605  sssnm  3785  prneimg  3805  dfiun2g  3949  exmidsssnc  4237  exmidundifim  4241  opth1  4270  copsexg  4278  opelopabt  4297  issod  4355  sowlin  4356  suctr  4457  reusv3i  4495  ralxfrALT  4503  ssorduni  4524  onintonm  4554  regexmidlem1  4570  nlimsucg  4603  0elnn  4656  issref  5053  iotaval  5231  fun11iun  5528  brprcneu  5554  fvssunirng  5576  relfvssunirn  5577  fv3  5584  ndmfvg  5592  ssimaex  5625  fvopab3ig  5638  dff4im  5711  ffnfv  5723  fconstfvm  5783  f1mpt  5821  oprabid  5957  mpoeq123  5985  f1o2ndf1  6295  brtposg  6321  rntpos  6324  dftpos4  6330  smores2  6361  tfri3  6434  rdgss  6450  nntri3or  6560  nndifsnid  6574  nnawordex  6596  eroveu  6694  map0g  6756  fundmen  6874  nneneq  6927  fiintim  7001  snon0  7010  fnfi  7011  infnlbti  7101  exmidonfinlem  7274  exmidontri2or  7328  addclpi  7413  enq0tr  7520  genprndl  7607  genprndu  7608  genpdisj  7609  addlocprlem  7621  nqprloc  7631  recexprlemss1l  7721  recexprlemss1u  7722  suplocexprlemss  7801  elrealeu  7915  ltleletr  8127  negf1o  8427  zletric  9389  zlelttric  9390  zltnle  9391  zmulcl  9398  zdcle  9421  zdclt  9422  zeo  9450  uz11  9643  indstr  9686  eqreznegel  9707  negm  9708  lbzbi  9709  fzdcel  10134  fzm1  10194  qletric  10350  qlelttric  10351  qltnle  10352  qdclt  10354  frecuzrdgtcl  10523  frecuzrdgfunlem  10530  qsqeqor  10761  rennim  11186  maxleast  11397  negfi  11412  fsum3cvg  11562  fproddccvg  11756  prodmodc  11762  ndvdssub  12114  bitsinv1lem  12145  algcvgblem  12244  algcvga  12246  isprm3  12313  oddprmdvds  12550  4sqlem2  12585  imasaddfnlemg  13018  subrngintm  13846  subrgintm  13877  lmodfopnelem1  13958  islssm  13991  lspsneq0  14060  islidlm  14113  epttop  14412  cnptoprest  14561  txcnp  14593  metequiv2  14818  cnlimcim  14993  bj-hbalt  15495  bj-intabssel1  15522  decidin  15529  sumdc2  15531  bj-charfunr  15542  bj-axemptylem  15624  bj-nnen2lp  15686  bj-nnord  15690  setindft  15697  bj-inf2vnlem2  15703  bj-inf2vnlem3  15704  bj-inf2vnlem4  15705  exmidsbthrlem  15757  triap  15764  tridceq  15791