Theorem ralimi 2595

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

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

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

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

This theorem is referenced by:  2ralimi  2596  ral2imi  2597  r19.26  2659  r19.29  2670  rr19.3v  2945  rr19.28v  2946  reu3  2996  uniiunlem  3316  reupick2  3493  uniss2  3924  ss2iun  3985  iineq2  3987  iunss2  4015  disjss2  4067  disjeq2  4068  disjnim  4078  repizf  4205  abnexg  4543  reusv3i  4556  tfis  4681  ssrel2  4816  issref  5119  dmmptg  5234  funco  5366  fununi  5398  fun11uni  5400  funimaexglem  5413  fnmpt  5459  fun11iun  5604  mpteqb  5737  chfnrn  5758  dffo5  5796  ffvresb  5810  fmptcof  5814  dfmptg  5827  mpo2eqb  6131  ralrnmpo  6136  rexrnmpo  6137  uchoice  6300  fnmpo  6367  mpoexxg  6375  smores  6458  riinerm  6777  ixpm  6899  difinfinf  7300  nninfwlpoimlemginf  7375  exmidontriimlem1  7436  onntri13  7456  onntri24  7460  cc4f  7488  cc4n  7490  cauappcvgprlemdisj  7871  caucvgsrlemasr  8010  caucvgsr  8022  suplocsr  8029  rexuz3  11552  recvguniq  11557  cau3lem  11676  caubnd2  11679  rexanre  11782  climi2  11850  climi0  11851  climcaucn  11913  ndvdssub  12493  gcdsupex  12530  gcdsupcl  12531  bezoutlemmo  12579  ptex  13349  mgmidmo  13457  issubg2m  13778  eltg2b  14781  neipsm  14881  lmcvg  14944  txlm  15006  metrest  15233  mulcncflem  15334  wlkvtxeledgg  16198  upgrwlkcompim  16216  upgrwlkvtxedg  16218  upgr2wlkdc  16231  bj-charfunbi  16423  bj-indint  16543  bj-indind  16544  bj-bdfindis  16559  setindis  16579  bdsetindis  16581  pw1dceq  16622  neap0mkv  16690