Theorem ralimi 2593

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

Syntax hints:   → wi 4   ∈ wcel 2200  ∀wral 2508

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1493  ax-gen 1495

This theorem depends on definitions:  df-bi 117  df-ral 2513

This theorem is referenced by:  2ralimi  2594  ral2imi  2595  r19.26  2657  r19.29  2668  rr19.3v  2942  rr19.28v  2943  reu3  2993  uniiunlem  3313  reupick2  3490  uniss2  3918  ss2iun  3979  iineq2  3981  iunss2  4009  disjss2  4061  disjeq2  4062  disjnim  4072  repizf  4199  abnexg  4536  reusv3i  4549  tfis  4674  ssrel2  4808  issref  5110  dmmptg  5225  funco  5357  fununi  5388  fun11uni  5390  funimaexglem  5403  fnmpt  5449  fun11iun  5592  mpteqb  5724  chfnrn  5745  dffo5  5783  ffvresb  5797  fmptcof  5801  dfmptg  5813  mpo2eqb  6113  ralrnmpo  6118  rexrnmpo  6119  uchoice  6281  fnmpo  6346  mpoexxg  6354  smores  6436  riinerm  6753  ixpm  6875  difinfinf  7264  nninfwlpoimlemginf  7339  exmidontriimlem1  7399  onntri13  7419  onntri24  7423  cc4f  7451  cc4n  7453  cauappcvgprlemdisj  7834  caucvgsrlemasr  7973  caucvgsr  7985  suplocsr  7992  rexuz3  11496  recvguniq  11501  cau3lem  11620  caubnd2  11623  rexanre  11726  climi2  11794  climi0  11795  climcaucn  11857  ndvdssub  12436  gcdsupex  12473  gcdsupcl  12474  bezoutlemmo  12522  ptex  13292  mgmidmo  13400  issubg2m  13721  eltg2b  14722  neipsm  14822  lmcvg  14885  txlm  14947  metrest  15174  mulcncflem  15275  wlkvtxeledgg  16041  bj-charfunbi  16132  bj-indint  16252  bj-indind  16253  bj-bdfindis  16268  setindis  16288  bdsetindis  16290  neap0mkv  16396