Theorem ralimia 3097

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  ∀wral 3077

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 3078

This theorem is used by:  ralimiaa  3099  ralimi  3100  rr19.3v  3621  rr19.28v  3622  exfo  7103  ffvresb  7124  f1mpt  7263  weniso  7362  xpord2indlem  8157  tz7.48lem  8443  ixpf  8941  ixpiunwdom  9577  tz9.12lem3  9789  dfac2a  10201  kmlem12  10233  axdc2lem  10519  ac6c4  10552  brdom6disj  10604  konigthlem  10646  arch  12596  cshw1  14966  serf0  15841  symgextfo  19629  baspartn  23265  ptcnplem  23933  spanuni  32139  lnopunilem1  32605  phpreu  38507  finixpnum  38508  poimirlem26  38544  indexa  38647  heiborlem5  38729  rngmgmbs4  38845  mzpincl  43724  dfac11  44048  mnurndlem1  45250  stgoldbwt  48843  2zrngnmlid2  49323