Theorem ralimi 2596

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

Syntax hints:   → wi 4   ∈ wcel 2202  ∀wral 2511

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 1496  ax-gen 1498

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

This theorem is referenced by:  2ralimi  2597  ral2imi  2598  r19.26  2660  r19.29  2671  rr19.3v  2946  rr19.28v  2947  reu3  2997  uniiunlem  3318  reupick2  3495  uniss2  3929  ss2iun  3990  iineq2  3992  iunss2  4020  disjss2  4072  disjeq2  4073  disjnim  4083  repizf  4210  abnexg  4549  reusv3i  4562  tfis  4687  ssrel2  4822  issref  5126  dmmptg  5241  funco  5373  fununi  5405  fun11uni  5407  funimaexglem  5420  fnmpt  5466  fun11iun  5613  mpteqb  5746  chfnrn  5767  dffo5  5804  ffvresb  5818  fmptcof  5822  dfmptg  5835  mpo2eqb  6141  ralrnmpo  6146  rexrnmpo  6147  uchoice  6309  fnmpo  6376  mpoexxg  6384  smores  6501  riinerm  6820  ixpm  6942  difinfinf  7343  nninfwlpoimlemginf  7418  exmidontriimlem1  7479  onntri13  7499  onntri24  7503  cc4f  7531  cc4n  7533  cauappcvgprlemdisj  7914  caucvgsrlemasr  8053  caucvgsr  8065  suplocsr  8072  rexuz3  11613  recvguniq  11618  cau3lem  11737  caubnd2  11740  rexanre  11843  climi2  11911  climi0  11912  climcaucn  11974  ndvdssub  12554  gcdsupex  12591  gcdsupcl  12592  bezoutlemmo  12640  ptex  13410  mgmidmo  13518  issubg2m  13839  eltg2b  14848  neipsm  14948  lmcvg  15011  txlm  15073  metrest  15300  mulcncflem  15401  wlkvtxeledgg  16268  upgrwlkcompim  16286  upgrwlkvtxedg  16288  upgr2wlkdc  16301  bj-charfunbi  16510  bj-indint  16630  bj-indind  16631  bj-bdfindis  16646  setindis  16666  bdsetindis  16668  pw1dceq  16709  exmidcon  16711  exmidpeirce  16712  neap0mkv  16785