Theorem r19.21bi 2593

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

Syntax hints:   → wi 4   ∧ wa 104  ∀wal 1370   ∈ wcel 2175  ∀wral 2483

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

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

This theorem is referenced by:  rspec2  2594  rspec3  2595  r19.21be  2596  frind  4398  wepo  4405  wetrep  4406  ordelord  4427  ralxfr2d  4510  rexxfr2d  4511  funfveu  5588  fvmptelcdm  5732  f1oresrab  5744  isoselem  5888  mpoexw  6298  disjxp1  6321  tfrlemisucaccv  6410  tfr1onlemsucaccv  6426  tfrcllemsucaccv  6439  xpf1o  6940  fimax2gtrilemstep  6996  supisoti  7111  difinfsn  7201  exmidomni  7243  cc3  7379  prcdnql  7596  prcunqu  7597  prdisj  7604  caucvgsrlembound  7906  caucvgsrlemoffgt1  7911  exbtwnzlemex  10390  monoord2  10629  iseqf1olemqk  10650  seq3f1olemqsumk  10655  caucvgrelemcau  11262  fimaxre2  11509  climrecvg1n  11630  zsumdc  11666  fsum3  11669  isumss2  11675  fsum3ser  11679  sumpr  11695  sumtp  11696  fsum2dlemstep  11716  fsumiun  11759  isumlessdc  11778  zproddc  11861  fprodsplitdc  11878  fprodcl2lem  11887  fprod2dlemstep  11904  bezoutlemstep  12289  ennnfonelemim  12766  ctiunctal  12783  prdsmndd  13251  grppropd  13320  srgdilem  13702  srgrz  13717  srglz  13718  cnmpt11  14726  psmet0  14770  psmettri2  14771  mulcncflem  15050  mulcncf  15051  dedekindeulemuub  15060  dedekindeulemlu  15064  dedekindicclemuub  15069  dedekindicclemlu  15073  limccnpcntop  15118  limccnp2lem  15119  limccnp2cntop  15120  plycoeid3  15200  fsumdvdsmul  15434  bj-charfundc  15706  bj-charfunbi  15709  nninffeq  15919  refeq  15929  iswomni0  15952  nconstwlpolem  15966