Theorem r19.21bi 2585

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

Syntax hints:   → wi 4   ∧ wa 104  ∀wal 1362   ∈ wcel 2167  ∀wral 2475

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

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

This theorem is referenced by:  rspec2  2586  rspec3  2587  r19.21be  2588  frind  4388  wepo  4395  wetrep  4396  ordelord  4417  ralxfr2d  4500  rexxfr2d  4501  funfveu  5574  fvmptelcdm  5718  f1oresrab  5730  isoselem  5870  mpoexw  6280  disjxp1  6303  tfrlemisucaccv  6392  tfr1onlemsucaccv  6408  tfrcllemsucaccv  6421  xpf1o  6914  fimax2gtrilemstep  6970  supisoti  7085  difinfsn  7175  exmidomni  7217  cc3  7353  prcdnql  7570  prcunqu  7571  prdisj  7578  caucvgsrlembound  7880  caucvgsrlemoffgt1  7885  exbtwnzlemex  10358  monoord2  10597  iseqf1olemqk  10618  seq3f1olemqsumk  10623  caucvgrelemcau  11164  fimaxre2  11411  climrecvg1n  11532  zsumdc  11568  fsum3  11571  isumss2  11577  fsum3ser  11581  sumpr  11597  sumtp  11598  fsum2dlemstep  11618  fsumiun  11661  isumlessdc  11680  zproddc  11763  fprodsplitdc  11780  fprodcl2lem  11789  fprod2dlemstep  11806  bezoutlemstep  12191  ennnfonelemim  12668  ctiunctal  12685  prdsmndd  13152  grppropd  13221  srgdilem  13603  srgrz  13618  srglz  13619  cnmpt11  14627  psmet0  14671  psmettri2  14672  mulcncflem  14951  mulcncf  14952  dedekindeulemuub  14961  dedekindeulemlu  14965  dedekindicclemuub  14970  dedekindicclemlu  14974  limccnpcntop  15019  limccnp2lem  15020  limccnp2cntop  15021  plycoeid3  15101  fsumdvdsmul  15335  bj-charfundc  15562  bj-charfunbi  15565  nninffeq  15775  refeq  15785  iswomni0  15808  nconstwlpolem  15822