Theorem ralimia 3100

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 15	. 2 ⊢ ((𝑥 ∈ 𝐴 → 𝜑) → (𝑥 ∈ 𝐴 → 𝜓))
3	2	ralimi2 3098	1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 𝜓)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147  ∀wral 3080

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842

This proof depends on definitions:  df-bi 210  df-ral 3081

This theorem is used by:  ralimiaa  3102  ralimi  3103  rr19.3v  3624  rr19.28v  3625  exfo  7137  ffvresb  7158  f1mpt  7296  weniso  7395  xpord2indlem  8201  tz7.48lem  8488  ixpf  8986  ixpiunwdom  9621  tz9.12lem3  9833  dfac2a  10247  kmlem12  10279  axdc2lem  10565  ac6c4  10598  brdom6disj  10650  konigthlem  10692  arch  12643  cshw1  15015  serf0  15892  symgextfo  19687  baspartn  23327  ptcnplem  23995  spanuni  32203  lnopunilem1  32669  ptpconn  36206  phpreu  38795  finixpnum  38796  poimirlem26  38832  indexa  38935  heiborlem5  39015  rngmgmbs4  39131  mzpincl  44011  dfac11  44330  mnurndlem1  45526  stgoldbwt  49147  2zrngnmlid2  49627