Theorem ralimi 2495

Description: Inference quantifying both antecedent and consequent, with strong hypothesis. (Contributed by NM, 4-Mar-1997.)

Hypothesis

Ref	Expression
ralimi.1	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
ralimi	⊢ (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 𝜓)

Proof of Theorem ralimi

Step	Hyp	Ref	Expression
1		ralimi.1	. . 3 ⊢ (𝜑 → 𝜓)
2	1	a1i 9	. 2 ⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓))
3	2	ralimia 2493	1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ∈ wcel 1480  ∀wral 2416

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425

This theorem depends on definitions:  df-bi 116  df-ral 2421

This theorem is referenced by:  2ralimi  2496  ral2imi  2497  r19.26  2558  r19.29  2569  rr19.3v  2823  rr19.28v  2824  reu3  2874  uniiunlem  3185  reupick2  3362  uniss2  3767  ss2iun  3828  iineq2  3830  iunss2  3858  disjss2  3909  disjeq2  3910  disjnim  3920  repizf  4044  abnexg  4367  reusv3i  4380  tfis  4497  ssrel2  4629  issref  4921  dmmptg  5036  funco  5163  fununi  5191  fun11uni  5193  funimaexglem  5206  fnmpt  5249  fun11iun  5388  mpteqb  5511  chfnrn  5531  dffo5  5569  ffvresb  5583  fmptcof  5587  dfmptg  5599  mpo2eqb  5880  ralrnmpo  5885  rexrnmpo  5886  fnmpo  6100  mpoexxg  6108  smores  6189  riinerm  6502  ixpm  6624  difinfinf  6986  cauappcvgprlemdisj  7459  caucvgsrlemasr  7598  caucvgsr  7610  suplocsr  7617  rexuz3  10762  recvguniq  10767  cau3lem  10886  caubnd2  10889  rexanre  10992  climi2  11057  climi0  11058  climcaucn  11120  ndvdssub  11627  gcdsupex  11646  gcdsupcl  11647  bezoutlemmo  11694  eltg2b  12223  neipsm  12323  lmcvg  12386  txlm  12448  metrest  12675  mulcncflem  12759  bj-indint  13129  bj-indind  13130  bj-bdfindis  13145  setindis  13165  bdsetindis  13167