Metamath Proof Explorer

Theorem a1i13

Description: Add two antecedents to a wff. (Contributed by Jeff Hankins, 4-Aug-2009)

Ref Expression
Hypothesis a1i13.1 
|- ( ps -> th )
Assertion a1i13 
|- ( ph -> ( ps -> ( ch -> th ) ) )

Proof

Step Hyp Ref Expression
1 a1i13.1 
 |-  ( ps -> th )
2 1 a1d 
 |-  ( ps -> ( ch -> th ) )
3 2 a1i 
 |-  ( ph -> ( ps -> ( ch -> th ) ) )