Metamath Proof Explorer


Theorem ralimdva

Description: Deduction quantifying both antecedent and consequent, based on Theorem 19.20 of Margaris p. 90. (Contributed by NM, 22-May-1999) Reduce dependencies on axioms. (Revised by Wolf Lammen, 5-Dec-2019)

Ref Expression
Hypothesis ralimdva.1 ( ( 𝜑𝑥𝐴 ) → ( 𝜓𝜒 ) )
Assertion ralimdva ( 𝜑 → ( ∀ 𝑥𝐴 𝜓 → ∀ 𝑥𝐴 𝜒 ) )

Proof

Step Hyp Ref Expression
1 ralimdva.1 ( ( 𝜑𝑥𝐴 ) → ( 𝜓𝜒 ) )
2 1 ex ( 𝜑 → ( 𝑥𝐴 → ( 𝜓𝜒 ) ) )
3 2 a2d ( 𝜑 → ( ( 𝑥𝐴𝜓 ) → ( 𝑥𝐴𝜒 ) ) )
4 3 ralimdv2 ( 𝜑 → ( ∀ 𝑥𝐴 𝜓 → ∀ 𝑥𝐴 𝜒 ) )