Theorem ralimia 3126

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

Syntax hints:   → wi 4   ∈ wcel 2111  ∀wral 3106

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

This theorem depends on definitions:  df-bi 210  df-ral 3111

This theorem is referenced by:  ralimiaa  3127  ralimi  3128  rr19.3v  3607  rr19.28v  3608  exfo  6848  ffvresb  6865  f1mpt  6997  weniso  7086  ixpf  8467  ixpiunwdom  9038  tz9.12lem3  9202  dfac2a  9540  kmlem12  9572  axdc2lem  9859  ac6c4  9892  brdom6disj  9943  konigthlem  9979  arch  11882  cshw1  14175  serf0  15029  symgextfo  18542  baspartn  21559  ptcnplem  22226  spanuni  29327  lnopunilem1  29793  phpreu  35041  finixpnum  35042  poimirlem26  35083  indexa  35171  heiborlem5  35253  rngmgmbs4  35369  mzpincl  39675  dfac11  40006  mnurndlem1  40989  stgoldbwt  44294  2zrngnmlid2  44575