Metamath Proof Explorer


Theorem ralimda

Description: Deduction quantifying both antecedent and consequent. (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses ralimda.1 𝑥 𝜑
ralimda.2 ( ( 𝜑𝑥𝐴 ) → ( 𝜓𝜒 ) )
Assertion ralimda ( 𝜑 → ( ∀ 𝑥𝐴 𝜓 → ∀ 𝑥𝐴 𝜒 ) )

Proof

Step Hyp Ref Expression
1 ralimda.1 𝑥 𝜑
2 ralimda.2 ( ( 𝜑𝑥𝐴 ) → ( 𝜓𝜒 ) )
3 nfra1 𝑥𝑥𝐴 𝜓
4 1 3 nfan 𝑥 ( 𝜑 ∧ ∀ 𝑥𝐴 𝜓 )
5 id ( ( 𝜑𝑥𝐴 ) → ( 𝜑𝑥𝐴 ) )
6 5 adantlr ( ( ( 𝜑 ∧ ∀ 𝑥𝐴 𝜓 ) ∧ 𝑥𝐴 ) → ( 𝜑𝑥𝐴 ) )
7 rspa ( ( ∀ 𝑥𝐴 𝜓𝑥𝐴 ) → 𝜓 )
8 7 adantll ( ( ( 𝜑 ∧ ∀ 𝑥𝐴 𝜓 ) ∧ 𝑥𝐴 ) → 𝜓 )
9 6 8 2 sylc ( ( ( 𝜑 ∧ ∀ 𝑥𝐴 𝜓 ) ∧ 𝑥𝐴 ) → 𝜒 )
10 4 9 ralrimia ( ( 𝜑 ∧ ∀ 𝑥𝐴 𝜓 ) → ∀ 𝑥𝐴 𝜒 )
11 10 ex ( 𝜑 → ( ∀ 𝑥𝐴 𝜓 → ∀ 𝑥𝐴 𝜒 ) )