Theorem ralimia 3070

Description: Inference quantifying both antecedent and consequent. (Contributed by NM, 19-Jul-1996.)

Hypothesis

Ref	Expression
ralimia.1	⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓))

Assertion

Ref	Expression
ralimia	⊢ (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 𝜓)

Proof of Theorem ralimia

Step	Hyp	Ref	Expression
1		ralimia.1	. . 3 ⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓))
2	1	a2i 14	. 2 ⊢ ((𝑥 ∈ 𝐴 → 𝜑) → (𝑥 ∈ 𝐴 → 𝜓))
3	2	ralimi2 3068	1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ∈ wcel 2108  ∀wral 3051

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809

This theorem depends on definitions:  df-bi 207  df-ral 3052

This theorem is referenced by:  ralimiaa  3072  ralimi  3073  rr19.3v  3646  rr19.28v  3647  exfo  7095  ffvresb  7115  f1mpt  7254  weniso  7347  xpord2indlem  8146  ixpf  8934  ixpiunwdom  9604  tz9.12lem3  9803  dfac2a  10144  kmlem12  10176  axdc2lem  10462  ac6c4  10495  brdom6disj  10546  konigthlem  10582  arch  12498  cshw1  14840  serf0  15697  symgextfo  19403  baspartn  22892  ptcnplem  23559  spanuni  31525  lnopunilem1  31991  phpreu  37628  finixpnum  37629  poimirlem26  37670  indexa  37757  heiborlem5  37839  rngmgmbs4  37955  mzpincl  42757  dfac11  43086  mnurndlem1  44305  natlocalincr  46905  stgoldbwt  47790  2zrngnmlid2  48232