Theorem ralimia 3096

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  ∀wral 3076

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841

This proof depends on definitions:  df-bi 210  df-ral 3077

This theorem is used by:  ralimiaa  3098  ralimi  3099  rr19.3v  3620  rr19.28v  3621  exfo  7106  ffvresb  7127  f1mpt  7266  weniso  7365  xpord2indlem  8167  tz7.48lem  8454  ixpf  8952  ixpiunwdom  9588  tz9.12lem3  9800  dfac2a  10212  kmlem12  10244  axdc2lem  10530  ac6c4  10563  brdom6disj  10615  konigthlem  10657  arch  12607  cshw1  14978  serf0  15854  symgextfo  19642  baspartn  23278  ptcnplem  23946  spanuni  32152  lnopunilem1  32618  ptpconn  36085  phpreu  38621  finixpnum  38622  poimirlem26  38658  indexa  38761  heiborlem5  38843  rngmgmbs4  38959  mzpincl  43839  dfac11  44158  mnurndlem1  45359  stgoldbwt  48968  2zrngnmlid2  49448