Theorem ralimia 3091

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

Syntax hints:   → wi 4   ∈ wcel 2112  ∀wral 3071

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

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

This theorem is referenced by:  ralimiaa  3092  ralimi  3093  rr19.3v  3583  rr19.28v  3584  exfo  6869  ffvresb  6886  f1mpt  7018  weniso  7108  ixpf  8516  ixpiunwdom  9101  tz9.12lem3  9265  dfac2a  9603  kmlem12  9635  axdc2lem  9922  ac6c4  9955  brdom6disj  10006  konigthlem  10042  arch  11945  cshw1  14245  serf0  15099  symgextfo  18632  baspartn  21669  ptcnplem  22336  spanuni  29441  lnopunilem1  29907  xpord2ind  33363  xpord3ind  33369  phpreu  35357  finixpnum  35358  poimirlem26  35399  indexa  35487  heiborlem5  35569  rngmgmbs4  35685  mzpincl  40094  dfac11  40425  mnurndlem1  41408  stgoldbwt  44721  2zrngnmlid2  45002