Theorem r19.21bi 2582

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

Syntax hints:   → wi 4   ∧ wa 104  ∀wal 1362   ∈ wcel 2164  ∀wral 2472

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

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

This theorem is referenced by:  rspec2  2583  rspec3  2584  r19.21be  2585  frind  4384  wepo  4391  wetrep  4392  ordelord  4413  ralxfr2d  4496  rexxfr2d  4497  funfveu  5568  fvmptelcdm  5712  f1oresrab  5724  isoselem  5864  mpoexw  6268  disjxp1  6291  tfrlemisucaccv  6380  tfr1onlemsucaccv  6396  tfrcllemsucaccv  6409  xpf1o  6902  fimax2gtrilemstep  6958  supisoti  7071  difinfsn  7161  exmidomni  7203  cc3  7330  prcdnql  7546  prcunqu  7547  prdisj  7554  caucvgsrlembound  7856  caucvgsrlemoffgt1  7861  exbtwnzlemex  10321  monoord2  10560  iseqf1olemqk  10581  seq3f1olemqsumk  10586  caucvgrelemcau  11127  fimaxre2  11373  climrecvg1n  11494  zsumdc  11530  fsum3  11533  isumss2  11539  fsum3ser  11543  sumpr  11559  sumtp  11560  fsum2dlemstep  11580  fsumiun  11623  isumlessdc  11642  zproddc  11725  fprodsplitdc  11742  fprodcl2lem  11751  fprod2dlemstep  11768  bezoutlemstep  12137  ennnfonelemim  12584  ctiunctal  12601  grppropd  13092  srgdilem  13468  srgrz  13483  srglz  13484  cnmpt11  14462  psmet0  14506  psmettri2  14507  mulcncflem  14786  mulcncf  14787  dedekindeulemuub  14796  dedekindeulemlu  14800  dedekindicclemuub  14805  dedekindicclemlu  14809  limccnpcntop  14854  limccnp2lem  14855  limccnp2cntop  14856  bj-charfundc  15370  bj-charfunbi  15373  nninffeq  15580  refeq  15588  iswomni0  15611  nconstwlpolem  15625