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  4383  wepo  4390  wetrep  4391  ordelord  4412  ralxfr2d  4495  rexxfr2d  4496  funfveu  5567  fvmptelcdm  5711  f1oresrab  5723  isoselem  5863  mpoexw  6266  disjxp1  6289  tfrlemisucaccv  6378  tfr1onlemsucaccv  6394  tfrcllemsucaccv  6407  xpf1o  6900  fimax2gtrilemstep  6956  supisoti  7069  difinfsn  7159  exmidomni  7201  cc3  7328  prcdnql  7544  prcunqu  7545  prdisj  7552  caucvgsrlembound  7854  caucvgsrlemoffgt1  7859  exbtwnzlemex  10318  monoord2  10557  iseqf1olemqk  10578  seq3f1olemqsumk  10583  caucvgrelemcau  11124  fimaxre2  11370  climrecvg1n  11491  zsumdc  11527  fsum3  11530  isumss2  11536  fsum3ser  11540  sumpr  11556  sumtp  11557  fsum2dlemstep  11577  fsumiun  11620  isumlessdc  11639  zproddc  11722  fprodsplitdc  11739  fprodcl2lem  11748  fprod2dlemstep  11765  bezoutlemstep  12134  ennnfonelemim  12581  ctiunctal  12598  grppropd  13089  srgdilem  13465  srgrz  13480  srglz  13481  cnmpt11  14451  psmet0  14495  psmettri2  14496  mulcncflem  14761  mulcncf  14762  dedekindeulemuub  14771  dedekindeulemlu  14775  dedekindicclemuub  14780  dedekindicclemlu  14784  limccnpcntop  14829  limccnp2lem  14830  limccnp2cntop  14831  bj-charfundc  15300  bj-charfunbi  15303  nninffeq  15510  refeq  15518  iswomni0  15541  nconstwlpolem  15555