Theorem ralimi 2560

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

Syntax hints:   → wi 4   ∈ wcel 2167  ∀wral 2475

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 1461  ax-gen 1463

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

This theorem is referenced by:  2ralimi  2561  ral2imi  2562  r19.26  2623  r19.29  2634  rr19.3v  2903  rr19.28v  2904  reu3  2954  uniiunlem  3273  reupick2  3450  uniss2  3871  ss2iun  3932  iineq2  3934  iunss2  3962  disjss2  4014  disjeq2  4015  disjnim  4025  repizf  4150  abnexg  4482  reusv3i  4495  tfis  4620  ssrel2  4754  issref  5053  dmmptg  5168  funco  5299  fununi  5327  fun11uni  5329  funimaexglem  5342  fnmpt  5387  fun11iun  5528  mpteqb  5655  chfnrn  5676  dffo5  5714  ffvresb  5728  fmptcof  5732  dfmptg  5744  mpo2eqb  6036  ralrnmpo  6041  rexrnmpo  6042  uchoice  6204  fnmpo  6269  mpoexxg  6277  smores  6359  riinerm  6676  ixpm  6798  difinfinf  7176  nninfwlpoimlemginf  7251  exmidontriimlem1  7306  onntri13  7323  onntri24  7327  cc4f  7354  cc4n  7356  cauappcvgprlemdisj  7737  caucvgsrlemasr  7876  caucvgsr  7888  suplocsr  7895  rexuz3  11174  recvguniq  11179  cau3lem  11298  caubnd2  11301  rexanre  11404  climi2  11472  climi0  11473  climcaucn  11535  ndvdssub  12114  gcdsupex  12151  gcdsupcl  12152  bezoutlemmo  12200  ptex  12968  mgmidmo  13076  issubg2m  13397  eltg2b  14398  neipsm  14498  lmcvg  14561  txlm  14623  metrest  14850  mulcncflem  14951  bj-charfunbi  15565  bj-indint  15685  bj-indind  15686  bj-bdfindis  15701  setindis  15721  bdsetindis  15723  neap0mkv  15826