Metamath Proof Explorer

Theorem a1i

Description: Inference introducing an antecedent. Inference associated with ax-1 . Its associated inference is a1ii . See conventions for a definition of "associated inference". (Contributed by NM, 29-Dec-1992)

Ref Expression
Hypothesis a1i.1 φ
Assertion a1i ψ φ


Step Hyp Ref Expression
1 a1i.1 φ
2 ax-1 φ ψ φ
3 1 2 ax-mp ψ φ