Theorem ralimia 2934

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

Syntax hints:   → wi 4   ∈ wcel 1977  ∀wral 2896

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

This theorem depends on definitions:  df-bi 196  df-ral 2901

This theorem is referenced by:  ralimiaa  2935  ralimi  2936  r19.12  3045  rr19.3v  3314  rr19.28v  3315  exfo  6285  ffvresb  6301  f1mpt  6419  weniso  6504  ixpf  7816  ixpiunwdom  8379  tz9.12lem3  8535  dfac2a  8835  kmlem12  8866  axdc2lem  9153  ac6num  9184  ac6c4  9186  brdom6disj  9235  konigthlem  9269  arch  11166  cshw1  13419  serf0  14259  symgextfo  17665  baspartn  20569  ptcnplem  21234  spanuni  27787  lnopunilem1  28253  phpreu  32563  finixpnum  32564  poimirlem26  32605  indexa  32698  heiborlem5  32784  rngmgmbs4  32900  mzpincl  36315  dfac11  36650  stgoldbwt  40198  2zrngnmlid2  41741