This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem bj-alrimd

Description: A slightly more general alrimd . A common usage will have ph substituted for ps and ch substituted for th , giving a form closer to alrimd . (Contributed by BJ, 25-Dec-2023)

	Ref	Expression
Hypotheses	bj-alrimd.ph	$⊢ φ \to \forall x ψ$
	bj-alrimd.th	$⊢ φ \to (χ \to \forall x θ)$
	bj-alrimd.maj	$⊢ ψ \to (θ \to τ)$
Assertion	bj-alrimd	$⊢ φ \to (χ \to \forall x τ)$

Proof

Step	Hyp	Ref	Expression
1		bj-alrimd.ph	$⊢ φ \to \forall x ψ$
2		bj-alrimd.th	$⊢ φ \to (χ \to \forall x θ)$
3		bj-alrimd.maj	$⊢ ψ \to (θ \to τ)$
4	1 3	sylg	$⊢ φ \to \forall x (θ \to τ)$
5		bj-alrimg	$⊢ (χ \to \forall x θ) \to (\forall x (θ \to τ) \to (χ \to \forall x τ))$
6	2 4 5	sylc	$⊢ φ \to (χ \to \forall x τ)$