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 ( 𝜑 → ( 𝜓 → ( 𝜒𝜑 ) ) )

Proof

Step Hyp Ref Expression
1 id ( 𝜑𝜑 )
2 1 2a1d ( 𝜑 → ( 𝜓 → ( 𝜒𝜑 ) ) )