Theorem syl3d 26

Description: Deduction adding nested antecedents.

Hypothesis

Ref	Expression
syl3d.1	|- (ph -> (ps -> ch))

Assertion

Ref	Expression
syl3d	|- (ph -> ((th -> ps) -> (th -> ch)))

Proof of Theorem syl3d

Step	Hyp	Ref	Expression
1		syl3d.1	. . 3 |- (ph -> (ps -> ch))
2	1	a1d 14	. 2 |- (ph -> (th -> (ps -> ch)))
3	2	a2d 15	1 |- (ph -> ((th -> ps) -> (th -> ch)))

Syntax hints:   -> wi 2

This theorem is referenced by:  syld 27  syl34d 29  syl6d 54  anc2l 248  anc2r 249  prth 429  dedlem0b 568  meredith 644  19.21g 792  ssuni 1937  omordi 3164  omsmolem 3195  r1ord 3499  aceq5 3563  aceq6a 3564  alephordi 3679  suppsr3 4018  nnsub 4450  occllem6 5185  projlem25 5217  osumlem4 5533  mdsymlem6 5781

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-mp 6

metamath.org