Theorem ralimia 3086

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

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

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

This theorem depends on definitions:  df-bi 206  df-ral 3070

This theorem is referenced by:  ralimiaa  3087  ralimi  3088  rr19.3v  3599  rr19.28v  3600  exfo  6975  ffvresb  6992  f1mpt  7128  weniso  7218  ixpf  8682  ixpiunwdom  9310  tz9.12lem3  9531  dfac2a  9869  kmlem12  9901  axdc2lem  10188  ac6c4  10221  brdom6disj  10272  konigthlem  10308  arch  12213  cshw1  14516  serf0  15373  symgextfo  19011  baspartn  22085  ptcnplem  22753  spanuni  29885  lnopunilem1  30351  xpord2ind  33773  xpord3ind  33779  phpreu  35740  finixpnum  35741  poimirlem26  35782  indexa  35870  heiborlem5  35952  rngmgmbs4  36068  mzpincl  40536  dfac11  40867  mnurndlem1  41852  stgoldbwt  45180  2zrngnmlid2  45461