This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database SUPPLEMENTARY MATERIAL (USERS' MATHBOXES) Mathbox for BJ First-order logic Adding ax-4 bj-exalimsi
Description: An inference for distributing quantifiers over a nested implication.
(Almost) the general statement that spimfw proves. (Contributed by BJ , 29-Sep-2019)
Ref
Expression
Hypotheses
bj-exalimsi.1 ⊢ ( 𝜑 → ( 𝜓 → 𝜒 ) )
bj-exalimsi.2 ⊢ ( ∃ 𝑥 𝜑 → ( ¬ 𝜒 → ∀ 𝑥 ¬ 𝜒 ) )
Assertion
bj-exalimsi ⊢ ( ∃ 𝑥 𝜑 → ( ∀ 𝑥 𝜓 → 𝜒 ) )
Proof
Step
Hyp
Ref
Expression
1
bj-exalimsi.1 ⊢ ( 𝜑 → ( 𝜓 → 𝜒 ) )
2
bj-exalimsi.2 ⊢ ( ∃ 𝑥 𝜑 → ( ¬ 𝜒 → ∀ 𝑥 ¬ 𝜒 ) )
3
2
bj-exalims ⊢ ( ∀ 𝑥 ( 𝜑 → ( 𝜓 → 𝜒 ) ) → ( ∃ 𝑥 𝜑 → ( ∀ 𝑥 𝜓 → 𝜒 ) ) )
4
3 1
mpg ⊢ ( ∃ 𝑥 𝜑 → ( ∀ 𝑥 𝜓 → 𝜒 ) )