Theorem r19.21bi 2618

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

Syntax hints:   → wi 4   ∧ wa 104  ∀wal 1393   ∈ wcel 2200  ∀wral 2508

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

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

This theorem is referenced by:  rspec2  2619  rspec3  2620  r19.21be  2621  frind  4443  wepo  4450  wetrep  4451  ordelord  4472  ralxfr2d  4555  rexxfr2d  4556  funfveu  5642  fvmptelcdm  5790  f1oresrab  5802  isoselem  5950  mpoexw  6365  disjxp1  6388  tfrlemisucaccv  6477  tfr1onlemsucaccv  6493  tfrcllemsucaccv  6506  xpf1o  7013  fimax2gtrilemstep  7071  supisoti  7188  difinfsn  7278  exmidomni  7320  cc3  7465  prcdnql  7682  prcunqu  7683  prdisj  7690  caucvgsrlembound  7992  caucvgsrlemoffgt1  7997  exbtwnzlemex  10481  monoord2  10720  iseqf1olemqk  10741  seq3f1olemqsumk  10746  caucvgrelemcau  11506  fimaxre2  11753  climrecvg1n  11874  zsumdc  11910  fsum3  11913  isumss2  11919  fsum3ser  11923  sumpr  11939  sumtp  11940  fsum2dlemstep  11960  fsumiun  12003  isumlessdc  12022  zproddc  12105  fprodsplitdc  12122  fprodcl2lem  12131  fprod2dlemstep  12148  bezoutlemstep  12533  ennnfonelemim  13010  ctiunctal  13027  prdsmndd  13496  grppropd  13565  srgdilem  13947  srgrz  13962  srglz  13963  cnmpt11  14972  psmet0  15016  psmettri2  15017  mulcncflem  15296  mulcncf  15297  dedekindeulemuub  15306  dedekindeulemlu  15310  dedekindicclemuub  15315  dedekindicclemlu  15319  limccnpcntop  15364  limccnp2lem  15365  limccnp2cntop  15366  plycoeid3  15446  fsumdvdsmul  15680  bj-charfundc  16226  bj-charfunbi  16229  nninffeq  16446  refeq  16456  iswomni0  16479  nconstwlpolem  16493