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  3630  rr19.28v  3631  exfo  7059  ffvresb  7079  f1mpt  7218  weniso  7311  xpord2indlem  8103  ixpf  8870  ixpiunwdom  9519  tz9.12lem3  9718  dfac2a  10059  kmlem12  10091  axdc2lem  10377  ac6c4  10410  brdom6disj  10461  konigthlem  10497  arch  12415  cshw1  14763  serf0  15623  symgextfo  19328  baspartn  22817  ptcnplem  23484  spanuni  31446  lnopunilem1  31912  phpreu  37571  finixpnum  37572  poimirlem26  37613  indexa  37700  heiborlem5  37782  rngmgmbs4  37898  mzpincl  42695  dfac11  43024  mnurndlem1  44243  natlocalincr  46847  stgoldbwt  47750  2zrngnmlid2  48218