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  5961  mpoexw  6378  disjxp1  6401  tfrlemisucaccv  6491  tfr1onlemsucaccv  6507  tfrcllemsucaccv  6520  xpf1o  7030  fimax2gtrilemstep  7090  supisoti  7209  difinfsn  7299  exmidomni  7341  cc3  7487  prcdnql  7704  prcunqu  7705  prdisj  7712  caucvgsrlembound  8014  caucvgsrlemoffgt1  8019  exbtwnzlemex  10510  monoord2  10749  iseqf1olemqk  10770  seq3f1olemqsumk  10775  caucvgrelemcau  11545  fimaxre2  11792  climrecvg1n  11913  zsumdc  11950  fsum3  11953  isumss2  11959  fsum3ser  11963  sumpr  11979  sumtp  11980  fsum2dlemstep  12000  fsumiun  12043  isumlessdc  12062  zproddc  12145  fprodsplitdc  12162  fprodcl2lem  12171  fprod2dlemstep  12188  bezoutlemstep  12573  ennnfonelemim  13050  ctiunctal  13067  prdsmndd  13536  grppropd  13605  srgdilem  13988  srgrz  14003  srglz  14004  cnmpt11  15013  psmet0  15057  psmettri2  15058  mulcncflem  15337  mulcncf  15338  dedekindeulemuub  15347  dedekindeulemlu  15351  dedekindicclemuub  15356  dedekindicclemlu  15360  limccnpcntop  15405  limccnp2lem  15406  limccnp2cntop  15407  plycoeid3  15487  fsumdvdsmul  15721  bj-charfundc  16429  bj-charfunbi  16432  nninffeq  16648  refeq  16658  iswomni0  16682  nconstwlpolem  16696