Theorem r19.21bi 2585

Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 20-Nov-1994.)

Hypothesis

Ref	Expression
r19.21bi.1	⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓)

Assertion

Ref	Expression
r19.21bi	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝜓)

Proof of Theorem r19.21bi

Step	Hyp	Ref	Expression
1		r19.21bi.1	. . . 4 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓)
2		df-ral 2480	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜓))
3	1, 2	sylib 122	. . 3 ⊢ (𝜑 → ∀𝑥(𝑥 ∈ 𝐴 → 𝜓))
4	3	19.21bi 1572	. 2 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝜓))
5	4	imp 124	1 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 104  ∀wal 1362   ∈ wcel 2167  ∀wral 2475

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-4 1524

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

This theorem is referenced by:  rspec2  2586  rspec3  2587  r19.21be  2588  frind  4388  wepo  4395  wetrep  4396  ordelord  4417  ralxfr2d  4500  rexxfr2d  4501  funfveu  5574  fvmptelcdm  5718  f1oresrab  5730  isoselem  5870  mpoexw  6280  disjxp1  6303  tfrlemisucaccv  6392  tfr1onlemsucaccv  6408  tfrcllemsucaccv  6421  xpf1o  6914  fimax2gtrilemstep  6970  supisoti  7085  difinfsn  7175  exmidomni  7217  cc3  7351  prcdnql  7568  prcunqu  7569  prdisj  7576  caucvgsrlembound  7878  caucvgsrlemoffgt1  7883  exbtwnzlemex  10356  monoord2  10595  iseqf1olemqk  10616  seq3f1olemqsumk  10621  caucvgrelemcau  11162  fimaxre2  11409  climrecvg1n  11530  zsumdc  11566  fsum3  11569  isumss2  11575  fsum3ser  11579  sumpr  11595  sumtp  11596  fsum2dlemstep  11616  fsumiun  11659  isumlessdc  11678  zproddc  11761  fprodsplitdc  11778  fprodcl2lem  11787  fprod2dlemstep  11804  bezoutlemstep  12189  ennnfonelemim  12666  ctiunctal  12683  prdsmndd  13150  grppropd  13219  srgdilem  13601  srgrz  13616  srglz  13617  cnmpt11  14603  psmet0  14647  psmettri2  14648  mulcncflem  14927  mulcncf  14928  dedekindeulemuub  14937  dedekindeulemlu  14941  dedekindicclemuub  14946  dedekindicclemlu  14950  limccnpcntop  14995  limccnp2lem  14996  limccnp2cntop  14997  plycoeid3  15077  fsumdvdsmul  15311  bj-charfundc  15538  bj-charfunbi  15541  nninffeq  15751  refeq  15759  iswomni0  15782  nconstwlpolem  15796