Theorem syld 40

Description: Syllogism deduction. (Contributed by NM, 5-Aug-1993.) (Proof shortened by O'Cat, 19-Feb-2008.) (Proof shortened by Wolf Lammen, 3-Aug-2012.)

Notice that syld 40 has the same form as syl 15 with φ added in front of each hypothesis and conclusion. When all theorems referenced in a proof are converted in this way, we can replace φ with a hypothesis of the proof, allowing the hypothesis to be eliminated with id 19 and become an antecedent. The Deduction Theorem for propositional calculus, e.g. Theorem 3 in [Margaris] p. 56, tells us that this procedure is always possible.

Hypotheses

Ref	Expression
syld.1	⊢ (φ → (ψ → χ))
syld.2	⊢ (φ → (χ → θ))

Assertion

Ref	Expression
syld	⊢ (φ → (ψ → θ))

Proof of Theorem syld

Step	Hyp	Ref	Expression
1		syld.1	. 2 ⊢ (φ → (ψ → χ))
2		syld.2	. . 3 ⊢ (φ → (χ → θ))
3	2	a1d 22	. 2 ⊢ (φ → (ψ → (χ → θ)))
4	1, 3	mpdd 36	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:  3syld  51  sylsyld  52  nsyld  132  pm2.61d  150  sylibd  205  sylbid  206  sylibrd  225  sylbird  226  syland  467  alrimdd  1768  dvelimv  1939  ax10lem6  1943  dral1  1965  cbv1h  1978  sbied  2036  sbequi  2059  dral1-o  2154  ax11indalem  2197  ax11inda2ALT  2198  pwadjoin  4119  nnsucelr  4428  nndisjeq  4429  lenltfin  4469  ncfinlower  4483  tfin11  4493  evenodddisj  4516  nnadjoin  4520  nnpweq  4523  tfinnn  4534  sfinltfin  4535  vfintle  4546  vfinspsslem1  4550  eqfnfv  5392  ncssfin  6151  addccan2nc  6265  spacind  6287  nchoicelem9  6297  nchoicelem12  6300  nchoicelem17  6305  nchoicelem19  6307  fnfreclem3  6319  fnfrec  6320