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  5826  mpo2eqb  6130  ralrnmpo  6135  rexrnmpo  6136  uchoice  6299  fnmpo  6366  mpoexxg  6374  smores  6457  riinerm  6776  ixpm  6898  difinfinf  7299  nninfwlpoimlemginf  7374  exmidontriimlem1  7435  onntri13  7455  onntri24  7459  cc4f  7487  cc4n  7489  cauappcvgprlemdisj  7870  caucvgsrlemasr  8009  caucvgsr  8021  suplocsr  8028  rexuz3  11550  recvguniq  11555  cau3lem  11674  caubnd2  11677  rexanre  11780  climi2  11848  climi0  11849  climcaucn  11911  ndvdssub  12490  gcdsupex  12527  gcdsupcl  12528  bezoutlemmo  12576  ptex  13346  mgmidmo  13454  issubg2m  13775  eltg2b  14777  neipsm  14877  lmcvg  14940  txlm  15002  metrest  15229  mulcncflem  15330  wlkvtxeledgg  16194  upgrwlkcompim  16212  upgrwlkvtxedg  16214  upgr2wlkdc  16227  bj-charfunbi  16406  bj-indint  16526  bj-indind  16527  bj-bdfindis  16542  setindis  16562  bdsetindis  16564  pw1dceq  16605  neap0mkv  16673