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  6417  genprndl  6504  genprndu  6505  genpdisj  6506  addlocprlem  6518  nqprloc  6528  recexprlemss1l  6607  recexprlemss1u  6608  ltleletr  6897  zletric  8065  zlelttric  8066  zltnle  8067  zmulcl  8073  zdcle  8093  zdclt  8094  zeo  8119  uz11  8271  indstr  8312  eqreznegel  8325  negm  8326  lbzbi  8327  fzdcel  8674  fzm1  8732  frecuzrdgfn  8879  rennim  9211  bj-hbalt  9238  bj-intabssel1  9264  bj-axemptylem  9347  bj-nnen2lp  9414  bj-nnord  9418  setindft  9425  bj-inf2vnlem2  9431  bj-inf2vnlem3  9432  bj-inf2vnlem4  9433