Theorem ralimi 2540

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

Syntax hints:   → wi 4   ∈ wcel 2148  ∀wral 2455

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 1447  ax-gen 1449

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

This theorem is referenced by:  2ralimi  2541  ral2imi  2542  r19.26  2603  r19.29  2614  rr19.3v  2876  rr19.28v  2877  reu3  2927  uniiunlem  3244  reupick2  3421  uniss2  3840  ss2iun  3901  iineq2  3903  iunss2  3931  disjss2  3983  disjeq2  3984  disjnim  3994  repizf  4119  abnexg  4446  reusv3i  4459  tfis  4582  ssrel2  4716  issref  5011  dmmptg  5126  funco  5256  fununi  5284  fun11uni  5286  funimaexglem  5299  fnmpt  5342  fun11iun  5482  mpteqb  5606  chfnrn  5627  dffo5  5665  ffvresb  5679  fmptcof  5683  dfmptg  5695  mpo2eqb  5983  ralrnmpo  5988  rexrnmpo  5989  fnmpo  6202  mpoexxg  6210  smores  6292  riinerm  6607  ixpm  6729  difinfinf  7099  nninfwlpoimlemginf  7173  exmidontriimlem1  7219  onntri13  7236  onntri24  7240  cc4f  7267  cc4n  7269  cauappcvgprlemdisj  7649  caucvgsrlemasr  7788  caucvgsr  7800  suplocsr  7807  rexuz3  10998  recvguniq  11003  cau3lem  11122  caubnd2  11125  rexanre  11228  climi2  11295  climi0  11296  climcaucn  11358  ndvdssub  11934  gcdsupex  11957  gcdsupcl  11958  bezoutlemmo  12006  ptex  12712  mgmidmo  12790  issubg2m  13047  eltg2b  13524  neipsm  13624  lmcvg  13687  txlm  13749  metrest  13976  mulcncflem  14060  bj-charfunbi  14533  bj-indint  14653  bj-indind  14654  bj-bdfindis  14669  setindis  14689  bdsetindis  14691  neap0mkv  14786