Theorem ralimi 2613

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2209  ∀wral 2528

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502

This proof depends on definitions:  df-bi 117  df-ral 2533

This theorem is used by:  2ralimi  2614  ral2imi  2615  r19.26  2677  r19.29  2688  rr19.3v  2965  rr19.28v  2966  reu3  3016  uniiunlem  3338  reupick2  3519  rabxmdc  3554  uniss2  3966  ss2iun  4027  iineq2  4029  iunss2  4057  disjss2  4109  disjeq2  4110  disjnim  4120  repizf  4247  abnexg  4592  reusv3i  4605  tfis  4730  ssrel2  4865  issref  5170  dmmptg  5285  funco  5417  fununi  5449  fun11uni  5451  funimaexglem  5464  fnmpt  5510  fun11iun  5660  mpteqb  5796  chfnrn  5820  dffo5  5857  ffvresb  5871  fmptcof  5875  dfmptg  5888  mpo2eqb  6198  ralrnmpo  6203  rexrnmpo  6204  uchoice  6371  fnmpo  6438  mpoexxg  6446  smores  6563  riinerm  6882  ixpm  7012  difinfinf  7442  nninfwlpoimlemginf  7517  exmidontriimlem1  7578  onntri13  7598  onntri24  7602  cc4f  7636  cc4n  7638  cauappcvgprlemdisj  8019  caucvgsrlemasr  8158  caucvgsr  8170  suplocsr  8177  rexuz3  11772  recvguniq  11777  cau3lem  11897  caubnd2  11900  rexanre  12003  climi2  12073  climi0  12074  climcaucn  12136  ndvdssub  12716  gcdsupex  12753  gcdsupcl  12754  bezoutlemmo  12802  ptex  13671  mgmidmo  13745  issubg2m  14045  eltg2b  15246  neipsm  15346  lmcvg  15409  txlm  15471  metrest  15698  mulcncflem  15799  wlkvtxeledgg  16751  upgrwlkcompim  16769  upgrwlkvtxedg  16771  upgr2wlkdc  16784  bj-charfunbi  17003  bj-indint  17123  bj-indind  17124  bj-bdfindis  17139  setindis  17159  bdsetindis  17161  pw1dceq  17201  exmidcon  17203  exmidpeirce  17204  neap0mkv  17286