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 ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | id | |- ( ph -> ph ) |
|
| 2 | 1 | 2a1d | |- ( ph -> ( ps -> ( ch -> ph ) ) ) |