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  423  con2d  554  con3d  560  expi  566  pm5.21ndd  620  pm2.37  717  pm2.81  723  condc  748  con4biddc  753  dcim  783  pm2.54dc  789  pm4.79dc  808  pm2.85dc  810  pm3.12dc  864  dn1dc  866  3jao  1195  xoranor  1267  syl6an  1320  syl10  1321  hbald  1377  ax-12  1399  hbimd  1462  19.21ht  1470  19.30dc  1515  19.23t  1564  hbexd  1581  spimth  1620  spimed  1625  cbv2h  1631  equvini  1638  sbiedh  1667  sbcof2  1688  aev  1690  sb3  1709  hbsb2  1714  sbequilem  1716  sbft  1725  sbi1v  1768  cbvexdh  1798  mo23  1938  moexexdc  1981  euexex  1982  exists2  1994  dvelimdc  2194  rsp2  2365  rgen2a  2369  spcimgft  2623  spcimegft  2625  eueq3dc  2709  moeq3dc  2711  reu6  2724  ssddif  3165  reupick2  3217  sssnm  3516  prneimg  3536  dfiun2g  3680  opth1  3964  copsexg  3972  opelopabt  3990  issod  4047  sowlin  4048  suctr  4124  reusv3i  4157  ralxfrALT  4165  ssorduni  4179  regexmidlem1  4218  nlimsucg  4242  0elnn  4283  issref  4650  iotaval  4821  fun11iun  5090  brprcneu  5114  fvssunirng  5133  relfvssunirn  5134  fv3  5140  ndmfvg  5147  ssimaex  5177  fvopab3ig  5189  dff4im  5256  ffnfv  5266  fconstfvm  5322  f1mpt  5353  oprabid  5480  mpt2eq123  5506  f1o2ndf1  5791  brtposg  5810  rntpos  5813  dftpos4  5819  smores2  5850  tfr0  5878  tfri3  5894  rdgss  5910  rdgon  5913  nntri3or  6011  nnawordex  6037  eroveu  6133  fundmen  6222  addclpi  6311  enq0tr  6416  genprndl  6503  genprndu  6504  genpdisj  6505  addlocprlem  6517  nqprloc  6527  recexprlemss1l  6606  recexprlemss1u  6607  ltleletr  6877  zletric  8045  zlelttric  8046  zltnle  8047  zmulcl  8053  zdcle  8073  zdclt  8074  zeo  8099  uz11  8251  indstr  8292  eqreznegel  8305  negm  8306  lbzbi  8307  fzdcel  8654  fzm1  8712  frecuzrdgfn  8859  rennim  9191  bj-hbalt  9218  bj-intabssel1  9244  bj-nnen2lp  9388  setindft  9395  bj-inf2vnlem2  9401  bj-inf2vnlem3  9402  bj-inf2vnlem4  9403