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