Theorem r19.21bi 2632

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 2527	. . . 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 2205  ∀wral 2522

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 2527

This theorem is referenced by:  rspec2  2633  rspec3  2634  r19.21be  2635  frind  4478  wepo  4485  wetrep  4486  ordelord  4507  ralxfr2d  4590  rexxfr2d  4591  funfveu  5688  fvmptelcdm  5835  f1oresrab  5847  isoselem  5999  mpoexw  6422  disjxp1  6445  tfrlemisucaccv  6569  tfr1onlemsucaccv  6585  tfrcllemsucaccv  6598  xpf1o  7110  fimax2gtrilemstep  7171  supisoti  7314  difinfsn  7404  exmidomni  7446  cc3  7598  prcdnql  7815  prcunqu  7816  prdisj  7823  caucvgsrlembound  8125  caucvgsrlemoffgt1  8130  exbtwnzlemex  10633  monoord2  10872  iseqf1olemqk  10893  seq3f1olemqsumk  10898  caucvgrelemcau  11690  fimaxre2  11937  climrecvg1n  12058  zsumdc  12095  fsum3  12098  isumss2  12104  fsum3ser  12108  sumpr  12124  sumtp  12125  fsum2dlemstep  12145  fsumiun  12188  isumlessdc  12207  zproddc  12290  fprodsplitdc  12307  fprodcl2lem  12316  fprod2dlemstep  12333  bezoutlemstep  12718  ennnfonelemim  13259  ctiunctal  13276  grppropd  13772  prdsmndd  14136  srgdilem  14212  srgrz  14227  srglz  14228  psrbagcon  14952  cnmpt11  15274  psmet0  15318  psmettri2  15319  mulcncflem  15598  mulcncf  15599  dedekindeulemuub  15608  dedekindeulemlu  15612  dedekindicclemuub  15617  dedekindicclemlu  15621  limccnpcntop  15666  limccnp2lem  15667  limccnp2cntop  15668  plycoeid3  15748  fsumdvdsmul  15985  bj-charfundc  16704  bj-charfunbi  16707  nninffeq  16924  refeq  16934  iswomni0  16962  trimul0or  16971  nconstwlpolem  16977