Theorem ralimia 3080

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

Syntax hints:   → wi 4   ∈ wcel 2104  ∀wral 3062

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

This theorem depends on definitions:  df-bi 206  df-ral 3063

This theorem is referenced by:  ralimiaa  3082  ralimi  3083  rr19.3v  3603  rr19.28v  3604  exfo  7013  ffvresb  7030  f1mpt  7166  weniso  7257  ixpf  8739  ixpiunwdom  9393  tz9.12lem3  9591  dfac2a  9931  kmlem12  9963  axdc2lem  10250  ac6c4  10283  brdom6disj  10334  konigthlem  10370  arch  12276  cshw1  14580  serf0  15437  symgextfo  19075  baspartn  22149  ptcnplem  22817  spanuni  29951  lnopunilem1  30417  xpord2ind  33839  xpord3ind  33845  phpreu  35805  finixpnum  35806  poimirlem26  35847  indexa  35935  heiborlem5  36017  rngmgmbs4  36133  mzpincl  40593  dfac11  40925  mnurndlem1  41937  stgoldbwt  45286  2zrngnmlid2  45567  natlocalincr  46569