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 10	. 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 8

This theorem is referenced by:  syl56  30  syl6com  31  a1dd  42  syl6mpi  58  syl6c  60  com34  77  con1d  116  expi  141  looinv  174  syl6ib  217  syl6ibr  218  syl6bi  219  syl6bir  220  jaoi  368  pm2.37  817  pm2.81  824  oplem1  930  3jao  1243  ee12an  1363  ee23  1364  exlimdv  1636  spimfw  1646  hbald  1740  sp  1747  spOLD  1748  19.23t  1800  hbimdOLD  1816  nfaldOLD  1853  19.21tOLD  1863  ax12olem1  1927  ax12olem2  1928  ax10lem2  1937  ax10lem4  1941  ax10  1944  a16g  1945  spimt  1974  cbv1h  1978  cbv2h  1980  equvini  1987  sbft  2025  sbied  2036  sb3  2052  dfsb2  2055  hbsb2  2057  sbn  2062  sbi1  2063  sb9i  2094  sbal1  2126  aev-o  2182  ax11eq  2193  ax11el  2194  ax11indn  2195  ax11indi  2196  mo  2226  moexex  2273  2mo  2282  2eu1  2284  dvelimdc  2509  rsp2  2676  rgen2a  2680  mo2icl  3015  reu6  3025  reupick2  3541  pwpw0  3855  sssn  3864  pwsnALT  3882  dfiun2g  3999  iotaval  4350  nnsucelr  4428  nndisjeq  4429  ltfintri  4466  tfin11  4493  tfinnn  4534  vfinspss  4551  copsexg  4607  opelopabt  4699  xpcan  5057  xpcan2  5058  fun11iun  5305  fv3  5341  chfnrn  5399  dff3  5420  ffnfv  5427  fconstfv  5456  funsi  5520  oprabid  5550  mpt2eq123  5661  fundmen  6043  enmap2lem4  6066  enmap1lem4  6072  enprmaplem5  6080  leconnnc  6218  addceq0  6219  ncslesuc  6267  nchoicelem6  6294  nchoicelem12  6300  dmfrec  6316