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 ⊢ χ