Theorem r19.21bi 2621

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

Syntax hints:   → wi 4   ∧ wa 104  ∀wal 1396   ∈ wcel 2202  ∀wral 2511

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

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

This theorem is referenced by:  rspec2  2622  rspec3  2623  r19.21be  2624  frind  4455  wepo  4462  wetrep  4463  ordelord  4484  ralxfr2d  4567  rexxfr2d  4568  funfveu  5661  fvmptelcdm  5808  f1oresrab  5820  isoselem  5971  mpoexw  6387  disjxp1  6410  tfrlemisucaccv  6534  tfr1onlemsucaccv  6550  tfrcllemsucaccv  6563  xpf1o  7073  fimax2gtrilemstep  7133  supisoti  7252  difinfsn  7342  exmidomni  7384  cc3  7530  prcdnql  7747  prcunqu  7748  prdisj  7755  caucvgsrlembound  8057  caucvgsrlemoffgt1  8062  exbtwnzlemex  10555  monoord2  10794  iseqf1olemqk  10815  seq3f1olemqsumk  10820  caucvgrelemcau  11603  fimaxre2  11850  climrecvg1n  11971  zsumdc  12008  fsum3  12011  isumss2  12017  fsum3ser  12021  sumpr  12037  sumtp  12038  fsum2dlemstep  12058  fsumiun  12101  isumlessdc  12120  zproddc  12203  fprodsplitdc  12220  fprodcl2lem  12229  fprod2dlemstep  12246  bezoutlemstep  12631  ennnfonelemim  13108  ctiunctal  13125  prdsmndd  13594  grppropd  13663  srgdilem  14046  srgrz  14061  srglz  14062  psrbagcon  14755  cnmpt11  15077  psmet0  15121  psmettri2  15122  mulcncflem  15401  mulcncf  15402  dedekindeulemuub  15411  dedekindeulemlu  15415  dedekindicclemuub  15420  dedekindicclemlu  15424  limccnpcntop  15469  limccnp2lem  15470  limccnp2cntop  15471  plycoeid3  15551  fsumdvdsmul  15788  bj-charfundc  16507  bj-charfunbi  16510  nninffeq  16729  refeq  16739  iswomni0  16767  nconstwlpolem  16781