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  11771  recvguniq  11776  cau3lem  11896  caubnd2  11899  rexanre  12002  climi2  12072  climi0  12073  climcaucn  12135  ndvdssub  12715  gcdsupex  12752  gcdsupcl  12753  bezoutlemmo  12801  ptex  13669  mgmidmo  13743  issubg2m  14043  eltg2b  15207  neipsm  15307  lmcvg  15370  txlm  15432  metrest  15659  mulcncflem  15760  wlkvtxeledgg  16707  upgrwlkcompim  16725  upgrwlkvtxedg  16727  upgr2wlkdc  16740  bj-charfunbi  16959  bj-indint  17079  bj-indind  17080  bj-bdfindis  17095  setindis  17115  bdsetindis  17117  pw1dceq  17157  exmidcon  17159  exmidpeirce  17160  neap0mkv  17241