Theorem ralimi 2593

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

Syntax hints:   → wi 4   ∈ wcel 2200  ∀wral 2508

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 1493  ax-gen 1495

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

This theorem is referenced by:  2ralimi  2594  ral2imi  2595  r19.26  2657  r19.29  2668  rr19.3v  2942  rr19.28v  2943  reu3  2993  uniiunlem  3313  reupick2  3490  uniss2  3919  ss2iun  3980  iineq2  3982  iunss2  4010  disjss2  4062  disjeq2  4063  disjnim  4073  repizf  4200  abnexg  4537  reusv3i  4550  tfis  4675  ssrel2  4809  issref  5111  dmmptg  5226  funco  5358  fununi  5389  fun11uni  5391  funimaexglem  5404  fnmpt  5450  fun11iun  5595  mpteqb  5727  chfnrn  5748  dffo5  5786  ffvresb  5800  fmptcof  5804  dfmptg  5816  mpo2eqb  6120  ralrnmpo  6125  rexrnmpo  6126  uchoice  6289  fnmpo  6354  mpoexxg  6362  smores  6444  riinerm  6763  ixpm  6885  difinfinf  7279  nninfwlpoimlemginf  7354  exmidontriimlem1  7414  onntri13  7434  onntri24  7438  cc4f  7466  cc4n  7468  cauappcvgprlemdisj  7849  caucvgsrlemasr  7988  caucvgsr  8000  suplocsr  8007  rexuz3  11516  recvguniq  11521  cau3lem  11640  caubnd2  11643  rexanre  11746  climi2  11814  climi0  11815  climcaucn  11877  ndvdssub  12456  gcdsupex  12493  gcdsupcl  12494  bezoutlemmo  12542  ptex  13312  mgmidmo  13420  issubg2m  13741  eltg2b  14743  neipsm  14843  lmcvg  14906  txlm  14968  metrest  15195  mulcncflem  15296  wlkvtxeledgg  16085  upgrwlkcompim  16103  upgrwlkvtxedg  16105  upgr2wlkdc  16116  bj-charfunbi  16229  bj-indint  16349  bj-indind  16350  bj-bdfindis  16365  setindis  16385  bdsetindis  16387  pw1dceq  16429  neap0mkv  16497