Metamath Proof Explorer


Theorem 2a1

Description: A double form of ax-1 . Its associated inference is 2a1i . Its associated deduction is 2a1d . (Contributed by BJ, 10-Aug-2020) (Proof shortened by Wolf Lammen, 1-Sep-2020)

Ref Expression
Assertion 2a1
|- ( ph -> ( ps -> ( ch -> ph ) ) )

Proof

Step Hyp Ref Expression
1 id
 |-  ( ph -> ph )
2 1 2a1d
 |-  ( ph -> ( ps -> ( ch -> ph ) ) )