Theorem r19.21bi 2595

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

Syntax hints:   → wi 4   ∧ wa 104  ∀wal 1371   ∈ wcel 2177  ∀wral 2485

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

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

This theorem is referenced by:  rspec2  2596  rspec3  2597  r19.21be  2598  frind  4412  wepo  4419  wetrep  4420  ordelord  4441  ralxfr2d  4524  rexxfr2d  4525  funfveu  5607  fvmptelcdm  5751  f1oresrab  5763  isoselem  5907  mpoexw  6317  disjxp1  6340  tfrlemisucaccv  6429  tfr1onlemsucaccv  6445  tfrcllemsucaccv  6458  xpf1o  6961  fimax2gtrilemstep  7018  supisoti  7133  difinfsn  7223  exmidomni  7265  cc3  7410  prcdnql  7627  prcunqu  7628  prdisj  7635  caucvgsrlembound  7937  caucvgsrlemoffgt1  7942  exbtwnzlemex  10424  monoord2  10663  iseqf1olemqk  10684  seq3f1olemqsumk  10689  caucvgrelemcau  11376  fimaxre2  11623  climrecvg1n  11744  zsumdc  11780  fsum3  11783  isumss2  11789  fsum3ser  11793  sumpr  11809  sumtp  11810  fsum2dlemstep  11830  fsumiun  11873  isumlessdc  11892  zproddc  11975  fprodsplitdc  11992  fprodcl2lem  12001  fprod2dlemstep  12018  bezoutlemstep  12403  ennnfonelemim  12880  ctiunctal  12897  prdsmndd  13365  grppropd  13434  srgdilem  13816  srgrz  13831  srglz  13832  cnmpt11  14840  psmet0  14884  psmettri2  14885  mulcncflem  15164  mulcncf  15165  dedekindeulemuub  15174  dedekindeulemlu  15178  dedekindicclemuub  15183  dedekindicclemlu  15187  limccnpcntop  15232  limccnp2lem  15233  limccnp2cntop  15234  plycoeid3  15314  fsumdvdsmul  15548  bj-charfundc  15913  bj-charfunbi  15916  nninffeq  16129  refeq  16139  iswomni0  16162  nconstwlpolem  16176