Theorem ralimia 3066

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

Syntax hints:   → wi 4   ∈ wcel 2111  ∀wral 3047

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

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

This theorem is referenced by:  ralimiaa  3068  ralimi  3069  rr19.3v  3617  rr19.28v  3618  exfo  7033  ffvresb  7053  f1mpt  7190  weniso  7283  xpord2indlem  8072  ixpf  8839  ixpiunwdom  9471  tz9.12lem3  9677  dfac2a  10016  kmlem12  10048  axdc2lem  10334  ac6c4  10367  brdom6disj  10418  konigthlem  10454  arch  12373  cshw1  14724  serf0  15583  symgextfo  19329  baspartn  22864  ptcnplem  23531  spanuni  31516  lnopunilem1  31982  phpreu  37644  finixpnum  37645  poimirlem26  37686  indexa  37773  heiborlem5  37855  rngmgmbs4  37971  mzpincl  42767  dfac11  43095  mnurndlem1  44314  natlocalincr  46914  stgoldbwt  47807  2zrngnmlid2  48288