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  11233  fimaxre2  11480  climrecvg1n  11601  zsumdc  11637  fsum3  11640  isumss2  11646  fsum3ser  11650  sumpr  11666  sumtp  11667  fsum2dlemstep  11687  fsumiun  11730  isumlessdc  11749  zproddc  11832  fprodsplitdc  11849  fprodcl2lem  11858  fprod2dlemstep  11875  bezoutlemstep  12260  ennnfonelemim  12737  ctiunctal  12754  prdsmndd  13222  grppropd  13291  srgdilem  13673  srgrz  13688  srglz  13689  cnmpt11  14697  psmet0  14741  psmettri2  14742  mulcncflem  15021  mulcncf  15022  dedekindeulemuub  15031  dedekindeulemlu  15035  dedekindicclemuub  15040  dedekindicclemlu  15044  limccnpcntop  15089  limccnp2lem  15090  limccnp2cntop  15091  plycoeid3  15171  fsumdvdsmul  15405  bj-charfundc  15677  bj-charfunbi  15680  nninffeq  15890  refeq  15900  iswomni0  15923  nconstwlpolem  15937