Theorem ralimia 3131

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

Syntax hints:   → wi 4   ∈ wcel 2157  ∀wral 3089

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

This theorem depends on definitions:  df-bi 199  df-ral 3094

This theorem is referenced by:  ralimiaa  3132  ralimi  3133  r19.12  3244  rr19.3v  3535  rr19.28v  3536  exfo  6603  ffvresb  6620  f1mpt  6746  weniso  6832  ixpf  8170  ixpiunwdom  8738  tz9.12lem3  8902  dfac2a  9238  kmlem12  9271  axdc2lem  9558  ac6num  9589  ac6c4  9591  brdom6disj  9642  konigthlem  9678  arch  11577  cshw1  13907  serf0  14752  symgextfo  18154  baspartn  21087  ptcnplem  21753  spanuni  28928  lnopunilem1  29394  phpreu  33882  finixpnum  33883  poimirlem26  33924  indexa  34016  heiborlem5  34101  rngmgmbs4  34217  mzpincl  38079  dfac11  38413  stgoldbwt  42442  2zrngnmlid2  42746