This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem pm2.86d

Description: Deduction associated with pm2.86 . (Contributed by NM, 29-Jun-1995) (Proof shortened by Wolf Lammen, 3-Apr-2013)

Ref Expression
Hypothesis pm2.86d.1 
|- ( ph -> ( ( ps -> ch ) -> ( ps -> th ) ) )
Assertion pm2.86d 
|- ( ph -> ( ps -> ( ch -> th ) ) )

Proof

Step Hyp Ref Expression
1 pm2.86d.1 
 |-  ( ph -> ( ( ps -> ch ) -> ( ps -> th ) ) )
2 ax-1 
 |-  ( ch -> ( ps -> ch ) )
3 2 1 syl5 
 |-  ( ph -> ( ch -> ( ps -> th ) ) )
4 3 com23 
 |-  ( ph -> ( ps -> ( ch -> th ) ) )