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 | ⊢ ( 𝜑 → ( 𝜓 → ( 𝜒 → 𝜑 ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | id | ⊢ ( 𝜑 → 𝜑 ) | |
| 2 | 1 | 2a1d | ⊢ ( 𝜑 → ( 𝜓 → ( 𝜒 → 𝜑 ) ) ) |