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

Syntax hints:   → wi 4   ∈ wcel 2131  ∀wral 3042

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

This theorem depends on definitions:  df-bi 197  df-ral 3047

This theorem is referenced by:  ralimiaa  3081  ralimi  3082  r19.12  3193  rr19.3v  3477  rr19.28v  3478  exfo  6532  ffvresb  6549  f1mpt  6673  weniso  6759  ixpf  8088  ixpiunwdom  8653  tz9.12lem3  8817  dfac2a  9134  kmlem12  9167  axdc2lem  9454  ac6num  9485  ac6c4  9487  brdom6disj  9538  konigthlem  9574  arch  11473  cshw1  13760  serf0  14602  symgextfo  18034  baspartn  20952  ptcnplem  21618  spanuni  28704  lnopunilem1  29170  phpreu  33698  finixpnum  33699  poimirlem26  33740  indexa  33833  heiborlem5  33919  rngmgmbs4  34035  mzpincl  37791  dfac11  38126  stgoldbwt  42166  2zrngnmlid2  42453