Theorem ralimia 2950

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

Syntax hints:   → wi 4   ∈ wcel 1990  ∀wral 2912

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

This theorem depends on definitions:  df-bi 197  df-ral 2917

This theorem is referenced by:  ralimiaa  2951  ralimi  2952  r19.12  3063  rr19.3v  3345  rr19.28v  3346  exfo  6377  ffvresb  6394  f1mpt  6518  weniso  6604  ixpf  7930  ixpiunwdom  8496  tz9.12lem3  8652  dfac2a  8952  kmlem12  8983  axdc2lem  9270  ac6num  9301  ac6c4  9303  brdom6disj  9354  konigthlem  9390  arch  11289  cshw1  13568  serf0  14411  symgextfo  17842  baspartn  20758  ptcnplem  21424  spanuni  28403  lnopunilem1  28869  phpreu  33393  finixpnum  33394  poimirlem26  33435  indexa  33528  heiborlem5  33614  rngmgmbs4  33730  mzpincl  37297  dfac11  37632  stgoldbwt  41664  2zrngnmlid2  41951