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

Metamath Proof Explorer

Theorem aleximi

Description: A variant of al2imi : instead of applying A. x quantifiers to the final implication, replace them with E. x . A shorter proof is possible using nfa1 , sps and eximd , but it depends on more axioms. (Contributed by Wolf Lammen, 18-Aug-2019)

		Ref	Expression
	Hypothesis	aleximi.1	$⊢ φ \to (ψ \to χ)$
	Assertion	aleximi	$⊢ \forall x φ \to (\exists x ψ \to \exists x χ)$

Proof

Step	Hyp	Ref	Expression
1		aleximi.1	$⊢ φ \to (ψ \to χ)$
2	1	con3d	$⊢ φ \to (\neg χ \to \neg ψ)$
3	2	al2imi	$⊢ \forall x φ \to (\forall x \neg χ \to \forall x \neg ψ)$
4		alnex	$⊢ \forall x \neg χ \leftrightarrow \neg \exists x χ$
5		alnex	$⊢ \forall x \neg ψ \leftrightarrow \neg \exists x ψ$
6	3 4 5	3imtr3g	$⊢ \forall x φ \to (\neg \exists x χ \to \neg \exists x ψ)$
7	6	con4d	$⊢ \forall x φ \to (\exists x ψ \to \exists x χ)$