Metamath Proof Explorer


Theorem jarrii

Description: Inference associated with jarri . A consequence of ax-mp and ax-1 . (Contributed by SN, 14-Oct-2025)

Ref Expression
Hypotheses jarrii.1 ψ
jarrii.2 φ ψ χ
Assertion jarrii χ

Proof

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