Theorem ralimia 3096

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 15	. 2 ⊢ ((𝑥 ∈ 𝐴 → 𝜑) → (𝑥 ∈ 𝐴 → 𝜓))
3	2	ralimi2 3094	1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 𝜓)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  ∀wral 3076

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842

This proof depends on definitions:  df-bi 210  df-ral 3077

This theorem is used by:  ralimiaa  3098  ralimi  3099  rr19.3v  3621  rr19.28v  3622  exfo  7098  ffvresb  7119  f1mpt  7258  weniso  7357  xpord2indlem  8145  ixpf  8927  ixpiunwdom  9562  tz9.12lem3  9771  dfac2a  10132  kmlem12  10164  axdc2lem  10450  ac6c4  10483  brdom6disj  10535  konigthlem  10577  arch  12525  cshw1  14893  serf0  15768  symgextfo  19549  baspartn  23179  ptcnplem  23847  spanuni  32025  lnopunilem1  32491  phpreu  38358  finixpnum  38359  poimirlem26  38395  indexa  38483  heiborlem5  38565  rngmgmbs4  38681  mzpincl  43579  dfac11  43903  mnurndlem1  45105  stgoldbwt  48692  2zrngnmlid2  49172