Theorem syl6 29

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 25	1 ⊢ (φ → (ψ → θ))

Syntax hints:   → wi 4

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7

This theorem is referenced by:  syl56  30  syl6com  31  a1dd  42  syl6mpi  58  syl6c  60  com34  77  ex  108  syl6ib  150  syl6ibr  151  syl6bi  152  syl6bir  153  pm5.32d  426  con2d  542  con3d  548  expi  554  pm5.21ndd  608  pm2.37  705  pm2.81  711  condc  740  con4biddc  747  dcim  777  pm2.54dc  783  pm4.79dc  802  pm2.85dc  804  pm3.12dc  853  dn1dc  855  3jao  1182  xoranor  1253  ee12an  1302  ee23  1303  hbald  1361  ax-12  1383  hbimd  1447  19.21ht  1455  19.30dc  1500  19.23t  1549  hbexd  1566  spimth  1605  spimed  1610  cbv2h  1616  equvini  1623  sbiedh  1652  sbcof2  1673  aev  1675  sb3  1694  hbsb2  1699  sbequilem  1701  sbft  1710  sbi1v  1753  cbvexdh  1783  mo23  1923  moexexdc  1966  euexex  1967  exists2  1979  dvelimdc  2179  rsp2  2349  rgen2a  2353  spcimgft  2606  spcimegft  2608  eueq3dc  2692  moeq3dc  2694  reu6  2707  ssddif  3148  reupick2  3200  sssnm  3499  prneimg  3519  dfiun2g  3663  opth1  3947  copsexg  3955  opelopabt  3973  issod  4030  sowlin  4031  suctrALT  4107  reusv3i  4141  ralxfrALT  4149  ssorduni  4163  regexmidlem1  4202  nlimsucg  4226  0elnn  4267  issref  4634  iotaval  4805  fun11iun  5072  brprcneu  5096  fvssunirng  5115  relfvssunirn  5116  fv3  5122  ndmfvg  5129  ssimaex  5159  fvopab3ig  5171  dff4im  5238  ffnfv  5248  fconstfvm  5304  f1mpt  5335  oprabid  5461  mpt2eq123  5487  f1o2ndf1  5772  brtposg  5791  rntpos  5794  dftpos4  5800  smores2  5831  tfri3  5875  rdgss  5890  rdgon  5893  nntri3or  5987  nnawordex  6012  eroveu  6108  addclpi  6187  enq0tr  6289  genprndl  6376  genprndu  6377  genpdisj  6378  addlocprlem  6390  nqprloc  6400  recexprlemss1l  6469  recexprlemss1u  6470  ltleletr  6698  bj-hbalt  7157  bj-intabssel1  7183  bj-nnen2lp  7323  setindft  7330  bj-inf2vnlem2  7336  bj-inf2vnlem3  7337  bj-inf2vnlem4  7338