Theorem r19.21bi 2630

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 2525	. . . 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 2203  ∀wral 2520

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 2525

This theorem is referenced by:  rspec2  2631  rspec3  2632  r19.21be  2633  frind  4473  wepo  4480  wetrep  4481  ordelord  4502  ralxfr2d  4585  rexxfr2d  4586  funfveu  5683  fvmptelcdm  5830  f1oresrab  5842  isoselem  5993  mpoexw  6409  disjxp1  6432  tfrlemisucaccv  6556  tfr1onlemsucaccv  6572  tfrcllemsucaccv  6585  xpf1o  7097  fimax2gtrilemstep  7158  supisoti  7301  difinfsn  7391  exmidomni  7433  cc3  7582  prcdnql  7799  prcunqu  7800  prdisj  7807  caucvgsrlembound  8109  caucvgsrlemoffgt1  8114  exbtwnzlemex  10609  monoord2  10848  iseqf1olemqk  10869  seq3f1olemqsumk  10874  caucvgrelemcau  11665  fimaxre2  11912  climrecvg1n  12033  zsumdc  12070  fsum3  12073  isumss2  12079  fsum3ser  12083  sumpr  12099  sumtp  12100  fsum2dlemstep  12120  fsumiun  12163  isumlessdc  12182  zproddc  12265  fprodsplitdc  12282  fprodcl2lem  12291  fprod2dlemstep  12308  bezoutlemstep  12693  ennnfonelemim  13175  ctiunctal  13192  prdsmndd  13661  grppropd  13730  srgdilem  14113  srgrz  14128  srglz  14129  psrbagcon  14826  cnmpt11  15148  psmet0  15192  psmettri2  15193  mulcncflem  15472  mulcncf  15473  dedekindeulemuub  15482  dedekindeulemlu  15486  dedekindicclemuub  15491  dedekindicclemlu  15495  limccnpcntop  15540  limccnp2lem  15541  limccnp2cntop  15542  plycoeid3  15622  fsumdvdsmul  15859  bj-charfundc  16578  bj-charfunbi  16581  nninffeq  16798  refeq  16808  iswomni0  16836  trimul0or  16845  nconstwlpolem  16851