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  4249  abnexg  4594  reusv3i  4607  tfis  4732  ssrel2  4867  issref  5173  dmmptg  5288  funco  5420  fununi  5452  fun11uni  5454  funimaexglem  5467  fnmpt  5513  fun11iun  5663  mpteqb  5799  chfnrn  5823  dffo5  5860  ffvresb  5874  fmptcof  5878  dfmptg  5891  mpo2eqb  6201  ralrnmpo  6206  rexrnmpo  6207  uchoice  6375  fnmpo  6442  mpoexxg  6450  smores  6568  riinerm  6887  ixpm  7018  difinfinf  7447  nninfwlpoimlemginf  7522  exmidontriimlem1  7583  onntri13  7603  onntri24  7607  cc4f  7641  cc4n  7643  cauappcvgprlemdisj  8024  caucvgsrlemasr  8163  caucvgsr  8175  suplocsr  8182  rexuz3  11777  recvguniq  11782  cau3lem  11902  caubnd2  11905  rexanre  12008  climi2  12078  climi0  12079  climcaucn  12141  ndvdssub  12721  gcdsupex  12758  gcdsupcl  12759  bezoutlemmo  12807  ptex  13676  mgmidmo  13750  issubg2m  14050  eltg2b  15297  neipsm  15397  lmcvg  15460  txlm  15522  metrest  15749  mulcncflem  15850  wlkvtxeledgg  16807  upgrwlkcompim  16825  upgrwlkvtxedg  16827  upgr2wlkdc  16840  bj-charfunbi  17059  bj-indint  17179  bj-indind  17180  bj-bdfindis  17195  setindis  17215  bdsetindis  17217  pw1dceq  17257  exmidcon  17259  exmidpeirce  17260  neap0mkv  17343