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 ph added in front of each hypothesis and conclusion. When all theorems referenced in a proof are converted in this way, we can replace ph 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	|- (ph -> (ps -> ch))
syld.2	|- (ph -> (ch -> th))

Assertion

Ref	Expression
syld	|- (ph -> (ps -> th))

Proof of Theorem syld

Step	Hyp	Ref	Expression
1		syld.1	. 2 |- (ph -> (ps -> ch))
2		syld.2	. . 3 |- (ph -> (ch -> th))
3	2	a1d 22	. 2 |- (ph -> (ps -> (ch -> th)))
4	1, 3	mpdd 36	1 |- (ph -> (ps -> th))

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  4120  nnsucelr  4429  nndisjeq  4430  lenltfin  4470  ncfinlower  4484  tfin11  4494  evenodddisj  4517  nnadjoin  4521  nnpweq  4524  tfinnn  4535  sfinltfin  4536  vfintle  4547  vfinspsslem1  4551  eqfnfv  5393  ncssfin  6152  addccan2nc  6266  spacind  6288  nchoicelem9  6298  nchoicelem12  6301  nchoicelem17  6306  nchoicelem19  6308  fnfreclem3  6320  fnfrec  6321