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  11555  recvguniq  11560  cau3lem  11679  caubnd2  11682  rexanre  11785  climi2  11853  climi0  11854  climcaucn  11916  ndvdssub  12496  gcdsupex  12533  gcdsupcl  12534  bezoutlemmo  12582  ptex  13352  mgmidmo  13460  issubg2m  13781  eltg2b  14784  neipsm  14884  lmcvg  14947  txlm  15009  metrest  15236  mulcncflem  15337  wlkvtxeledgg  16201  upgrwlkcompim  16219  upgrwlkvtxedg  16221  upgr2wlkdc  16234  bj-charfunbi  16432  bj-indint  16552  bj-indind  16553  bj-bdfindis  16568  setindis  16588  bdsetindis  16590  pw1dceq  16631  neap0mkv  16700