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

Metamath Proof Explorer

Theorem bj-exlimd

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

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

Proof

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