Theorem ralimia 3160

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

Syntax hints:   → wi 4   ∈ wcel 2114  ∀wral 3140

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

This theorem depends on definitions:  df-bi 209  df-ral 3145

This theorem is referenced by:  ralimiaa  3161  ralimi  3162  r19.12OLD  3329  rr19.3v  3663  rr19.28v  3664  exfo  6873  ffvresb  6890  f1mpt  7021  weniso  7109  ixpf  8486  ixpiunwdom  9057  tz9.12lem3  9220  dfac2a  9557  kmlem12  9589  axdc2lem  9872  ac6c4  9905  brdom6disj  9956  konigthlem  9992  arch  11897  cshw1  14186  serf0  15039  symgextfo  18552  baspartn  21564  ptcnplem  22231  spanuni  29323  lnopunilem1  29789  phpreu  34878  finixpnum  34879  poimirlem26  34920  indexa  35010  heiborlem5  35095  rngmgmbs4  35211  mzpincl  39338  dfac11  39669  mnurndlem1  40624  stgoldbwt  43948  2zrngnmlid2  44229