Theorem ralimia 3067

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

Syntax hints:   → wi 4   ∈ wcel 2113  ∀wral 3048

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 3049

This theorem is referenced by:  ralimiaa  3069  ralimi  3070  rr19.3v  3618  rr19.28v  3619  exfo  7047  ffvresb  7067  f1mpt  7204  weniso  7297  xpord2indlem  8086  ixpf  8854  ixpiunwdom  9487  tz9.12lem3  9693  dfac2a  10032  kmlem12  10064  axdc2lem  10350  ac6c4  10383  brdom6disj  10434  konigthlem  10470  arch  12389  cshw1  14736  serf0  15595  symgextfo  19342  baspartn  22889  ptcnplem  23556  spanuni  31545  lnopunilem1  32011  phpreu  37717  finixpnum  37718  poimirlem26  37759  indexa  37846  heiborlem5  37928  rngmgmbs4  38044  mzpincl  42891  dfac11  43219  mnurndlem1  44438  natlocalincr  47036  stgoldbwt  47938  2zrngnmlid2  48419