Theorem r19.21bi 2462

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 2365	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜓))
3	1, 2	sylib 121	. . 3 ⊢ (𝜑 → ∀𝑥(𝑥 ∈ 𝐴 → 𝜓))
4	3	19.21bi 1496	. 2 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝜓))
5	4	imp 123	1 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 103  ∀wal 1288   ∈ wcel 1439  ∀wral 2360

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

This theorem depends on definitions:  df-bi 116  df-ral 2365

This theorem is referenced by:  rspec2  2463  rspec3  2464  r19.21be  2465  frind  4188  wepo  4195  wetrep  4196  ordelord  4217  ralxfr2d  4299  rexxfr2d  4300  funfveu  5331  f1oresrab  5477  isoselem  5613  disjxp1  6015  tfrlemisucaccv  6104  tfr1onlemsucaccv  6120  tfrcllemsucaccv  6133  xpf1o  6614  fimax2gtrilemstep  6670  supisoti  6759  exmidomni  6859  prcdnql  7104  prcunqu  7105  prdisj  7112  caucvgsrlembound  7400  caucvgsrlemoffgt1  7405  exbtwnzlemex  9722  monoord2  9966  iseqf1olemqk  9984  seq3f1olemqsumk  9989  caucvgrelemcau  10474  fimaxre2  10719  climrecvg1n  10798  zisum  10835  fisum  10839  isumss2  10846  fisumser  10851  sumpr  10868  sumtp  10869  fsum2dlemstep  10889  fsumiun  10932  isumlessdc  10951  bezoutlemstep  11325