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

Metamath Proof Explorer

Theorem reximdvai

Description: Deduction quantifying both antecedent and consequent, based on Theorem 19.22 of Margaris p. 90. (Contributed by NM, 14-Nov-2002) Reduce dependencies on axioms. (Revised by Wolf Lammen, 8-Jan-2020) (Proof shortened by Wolf Lammen, 4-Nov-2024)

Ref Expression
Hypothesis reximdvai.1 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 → ( 𝜓 → 𝜒 ) ) )
Assertion reximdvai ( 𝜑 → ( ∃ 𝑥 ∈ 𝐴 𝜓 → ∃ 𝑥 ∈ 𝐴 𝜒 ) )

Proof

Step Hyp Ref Expression
1 reximdvai.1 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 → ( 𝜓 → 𝜒 ) ) )
2 1 imdistand ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) → ( 𝑥 ∈ 𝐴 ∧ 𝜒 ) ) )
3 2 reximdv2 ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝐴 𝜓 → ∃ 𝑥 ∈ 𝐴 𝜒 ) )