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	⊢ ( 𝜑 → ( 𝜓 → 𝜒 ) )
	Assertion	aleximi	⊢ ( ∀ 𝑥 𝜑 → ( ∃ 𝑥 𝜓 → ∃ 𝑥 𝜒 ) )

Proof

Step	Hyp	Ref	Expression
1		aleximi.1	⊢ ( 𝜑 → ( 𝜓 → 𝜒 ) )
2	1	con3d	⊢ ( 𝜑 → ( ¬ 𝜒 → ¬ 𝜓 ) )
3	2	al2imi	⊢ ( ∀ 𝑥 𝜑 → ( ∀ 𝑥 ¬ 𝜒 → ∀ 𝑥 ¬ 𝜓 ) )
4		alnex	⊢ ( ∀ 𝑥 ¬ 𝜒 ↔ ¬ ∃ 𝑥 𝜒 )
5		alnex	⊢ ( ∀ 𝑥 ¬ 𝜓 ↔ ¬ ∃ 𝑥 𝜓 )
6	3 4 5	3imtr3g	⊢ ( ∀ 𝑥 𝜑 → ( ¬ ∃ 𝑥 𝜒 → ¬ ∃ 𝑥 𝜓 ) )
7	6	con4d	⊢ ( ∀ 𝑥 𝜑 → ( ∃ 𝑥 𝜓 → ∃ 𝑥 𝜒 ) )