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  2943  rr19.28v  2944  reu3  2994  uniiunlem  3314  reupick2  3491  uniss2  3922  ss2iun  3983  iineq2  3985  iunss2  4013  disjss2  4065  disjeq2  4066  disjnim  4076  repizf  4203  abnexg  4541  reusv3i  4554  tfis  4679  ssrel2  4814  issref  5117  dmmptg  5232  funco  5364  fununi  5395  fun11uni  5397  funimaexglem  5410  fnmpt  5456  fun11iun  5601  mpteqb  5733  chfnrn  5754  dffo5  5792  ffvresb  5806  fmptcof  5810  dfmptg  5822  mpo2eqb  6126  ralrnmpo  6131  rexrnmpo  6132  uchoice  6295  fnmpo  6362  mpoexxg  6370  smores  6453  riinerm  6772  ixpm  6894  difinfinf  7291  nninfwlpoimlemginf  7366  exmidontriimlem1  7426  onntri13  7446  onntri24  7450  cc4f  7478  cc4n  7480  cauappcvgprlemdisj  7861  caucvgsrlemasr  8000  caucvgsr  8012  suplocsr  8019  rexuz3  11541  recvguniq  11546  cau3lem  11665  caubnd2  11668  rexanre  11771  climi2  11839  climi0  11840  climcaucn  11902  ndvdssub  12481  gcdsupex  12518  gcdsupcl  12519  bezoutlemmo  12567  ptex  13337  mgmidmo  13445  issubg2m  13766  eltg2b  14768  neipsm  14868  lmcvg  14931  txlm  14993  metrest  15220  mulcncflem  15321  wlkvtxeledgg  16141  upgrwlkcompim  16159  upgrwlkvtxedg  16161  upgr2wlkdc  16172  bj-charfunbi  16342  bj-indint  16462  bj-indind  16463  bj-bdfindis  16478  setindis  16498  bdsetindis  16500  pw1dceq  16541  neap0mkv  16609