Theorem r19.21bi 2620

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 2515	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜓))
3	1, 2	sylib 122	. . 3 ⊢ (𝜑 → ∀𝑥(𝑥 ∈ 𝐴 → 𝜓))
4	3	19.21bi 1606	. 2 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝜓))
5	4	imp 124	1 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 104  ∀wal 1395   ∈ 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-4 1558

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

This theorem is referenced by:  rspec2  2621  rspec3  2622  r19.21be  2623  frind  4449  wepo  4456  wetrep  4457  ordelord  4478  ralxfr2d  4561  rexxfr2d  4562  funfveu  5652  fvmptelcdm  5800  f1oresrab  5812  isoselem  5960  mpoexw  6377  disjxp1  6400  tfrlemisucaccv  6490  tfr1onlemsucaccv  6506  tfrcllemsucaccv  6519  xpf1o  7029  fimax2gtrilemstep  7089  supisoti  7208  difinfsn  7298  exmidomni  7340  cc3  7486  prcdnql  7703  prcunqu  7704  prdisj  7711  caucvgsrlembound  8013  caucvgsrlemoffgt1  8018  exbtwnzlemex  10508  monoord2  10747  iseqf1olemqk  10768  seq3f1olemqsumk  10773  caucvgrelemcau  11540  fimaxre2  11787  climrecvg1n  11908  zsumdc  11944  fsum3  11947  isumss2  11953  fsum3ser  11957  sumpr  11973  sumtp  11974  fsum2dlemstep  11994  fsumiun  12037  isumlessdc  12056  zproddc  12139  fprodsplitdc  12156  fprodcl2lem  12165  fprod2dlemstep  12182  bezoutlemstep  12567  ennnfonelemim  13044  ctiunctal  13061  prdsmndd  13530  grppropd  13599  srgdilem  13981  srgrz  13996  srglz  13997  cnmpt11  15006  psmet0  15050  psmettri2  15051  mulcncflem  15330  mulcncf  15331  dedekindeulemuub  15340  dedekindeulemlu  15344  dedekindicclemuub  15349  dedekindicclemlu  15353  limccnpcntop  15398  limccnp2lem  15399  limccnp2cntop  15400  plycoeid3  15480  fsumdvdsmul  15714  bj-charfundc  16403  bj-charfunbi  16406  nninffeq  16622  refeq  16632  iswomni0  16655  nconstwlpolem  16669