Theorem ralimia 3063

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

Syntax hints:   → wi 4   ∈ wcel 2109  ∀wral 3044

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 3045

This theorem is referenced by:  ralimiaa  3065  ralimi  3066  rr19.3v  3633  rr19.28v  3634  exfo  7077  ffvresb  7097  f1mpt  7236  weniso  7329  xpord2indlem  8126  ixpf  8893  ixpiunwdom  9543  tz9.12lem3  9742  dfac2a  10083  kmlem12  10115  axdc2lem  10401  ac6c4  10434  brdom6disj  10485  konigthlem  10521  arch  12439  cshw1  14787  serf0  15647  symgextfo  19352  baspartn  22841  ptcnplem  23508  spanuni  31473  lnopunilem1  31939  phpreu  37598  finixpnum  37599  poimirlem26  37640  indexa  37727  heiborlem5  37809  rngmgmbs4  37925  mzpincl  42722  dfac11  43051  mnurndlem1  44270  natlocalincr  46874  stgoldbwt  47777  2zrngnmlid2  48245