Metamath Proof Explorer


Theorem bj-exalim

Description: Distribute quantifiers over a nested implication.

This and the following theorems are the general instances of already proved theorems. They could be moved to the main part, before ax-5 . I propose to move to the main part: bj-exalim , bj-exalimi , bj-exalims , bj-exalimsi , bj-ax12i , bj-ax12wlem , bj-ax12w . A new label is needed for bj-ax12i and label suggestions are welcome for the others. I also propose to change -. A. x -. to E. x in speimfw and spimfw (other spim* theorems use E. x and very few theorems in set.mm use -. A. x -. ). (Contributed by BJ, 8-Nov-2021)

Ref Expression
Assertion bj-exalim ( ∀ 𝑥 ( 𝜑 → ( 𝜓𝜒 ) ) → ( ∃ 𝑥 𝜑 → ( ∀ 𝑥 𝜓 → ∃ 𝑥 𝜒 ) ) )

Proof

Step Hyp Ref Expression
1 pm2.04 ( ( 𝜑 → ( 𝜓𝜒 ) ) → ( 𝜓 → ( 𝜑𝜒 ) ) )
2 1 alimi ( ∀ 𝑥 ( 𝜑 → ( 𝜓𝜒 ) ) → ∀ 𝑥 ( 𝜓 → ( 𝜑𝜒 ) ) )
3 bj-alexim ( ∀ 𝑥 ( 𝜓 → ( 𝜑𝜒 ) ) → ( ∀ 𝑥 𝜓 → ( ∃ 𝑥 𝜑 → ∃ 𝑥 𝜒 ) ) )
4 pm2.04 ( ( ∀ 𝑥 𝜓 → ( ∃ 𝑥 𝜑 → ∃ 𝑥 𝜒 ) ) → ( ∃ 𝑥 𝜑 → ( ∀ 𝑥 𝜓 → ∃ 𝑥 𝜒 ) ) )
5 2 3 4 3syl ( ∀ 𝑥 ( 𝜑 → ( 𝜓𝜒 ) ) → ( ∃ 𝑥 𝜑 → ( ∀ 𝑥 𝜓 → ∃ 𝑥 𝜒 ) ) )