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  3623  rr19.28v  3624  exfo  7059  ffvresb  7080  f1mpt  7217  weniso  7310  xpord2indlem  8099  ixpf  8870  ixpiunwdom  9507  tz9.12lem3  9713  dfac2a  10052  kmlem12  10084  axdc2lem  10370  ac6c4  10403  brdom6disj  10454  konigthlem  10491  arch  12410  cshw1  14757  serf0  15616  symgextfo  19363  baspartn  22910  ptcnplem  23577  spanuni  31631  lnopunilem1  32097  phpreu  37852  finixpnum  37853  poimirlem26  37894  indexa  37981  heiborlem5  38063  rngmgmbs4  38179  mzpincl  43088  dfac11  43416  mnurndlem1  44634  natlocalincr  47231  stgoldbwt  48133  2zrngnmlid2  48614