Theorem ralimia 3099

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

Syntax hints:   → wi 4   ∈ wcel 2143  ∀wral 3079

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

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

This theorem is referenced by:  ralimiaa  3101  ralimi  3102  rr19.3v  3627  rr19.28v  3628  exfo  7102  ffvresb  7123  f1mpt  7261  weniso  7354  xpord2indlem  8144  ixpf  8919  ixpiunwdom  9553  tz9.12lem3  9762  dfac2a  10114  kmlem12  10146  axdc2lem  10433  ac6c4  10466  brdom6disj  10517  konigthlem  10554  arch  12502  cshw1  14861  serf0  15734  symgextfo  19493  baspartn  23092  ptcnplem  23759  spanuni  31877  lnopunilem1  32343  phpreu  38236  finixpnum  38237  poimirlem26  38278  indexa  38365  heiborlem5  38447  rngmgmbs4  38563  mzpincl  43448  dfac11  43772  mnurndlem1  44974  natlocalincr  47575  stgoldbwt  48524  2zrngnmlid2  49005