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	|- ps
	jarrii.2	|- ( ( ph -> ps ) -> ch )
Assertion	jarrii	|- ch

Proof

Step	Hyp	Ref	Expression
1		jarrii.1	|- ps
2		jarrii.2	|- ( ( ph -> ps ) -> ch )
3	1	a1i	|- ( ph -> ps )
4	3 2	ax-mp	|- ch