Theorem ralimia 3072

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 3070	1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ∈ wcel 2114  ∀wral 3052

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

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

This theorem is referenced by:  ralimiaa  3074  ralimi  3075  rr19.3v  3610  rr19.28v  3611  exfo  7051  ffvresb  7072  f1mpt  7209  weniso  7302  xpord2indlem  8090  ixpf  8861  ixpiunwdom  9498  tz9.12lem3  9704  dfac2a  10043  kmlem12  10075  axdc2lem  10361  ac6c4  10394  brdom6disj  10445  konigthlem  10482  arch  12425  cshw1  14775  serf0  15634  symgextfo  19388  baspartn  22929  ptcnplem  23596  spanuni  31630  lnopunilem1  32096  phpreu  37939  finixpnum  37940  poimirlem26  37981  indexa  38068  heiborlem5  38150  rngmgmbs4  38266  mzpincl  43180  dfac11  43508  mnurndlem1  44726  natlocalincr  47322  stgoldbwt  48264  2zrngnmlid2  48745