Theorem r19.21bi 2618

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

Syntax hints:   → wi 4   ∧ wa 104  ∀wal 1393   ∈ wcel 2200  ∀wral 2508

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

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

This theorem is referenced by:  rspec2  2619  rspec3  2620  r19.21be  2621  frind  4447  wepo  4454  wetrep  4455  ordelord  4476  ralxfr2d  4559  rexxfr2d  4560  funfveu  5648  fvmptelcdm  5796  f1oresrab  5808  isoselem  5956  mpoexw  6373  disjxp1  6396  tfrlemisucaccv  6486  tfr1onlemsucaccv  6502  tfrcllemsucaccv  6515  xpf1o  7025  fimax2gtrilemstep  7083  supisoti  7200  difinfsn  7290  exmidomni  7332  cc3  7477  prcdnql  7694  prcunqu  7695  prdisj  7702  caucvgsrlembound  8004  caucvgsrlemoffgt1  8009  exbtwnzlemex  10499  monoord2  10738  iseqf1olemqk  10759  seq3f1olemqsumk  10764  caucvgrelemcau  11531  fimaxre2  11778  climrecvg1n  11899  zsumdc  11935  fsum3  11938  isumss2  11944  fsum3ser  11948  sumpr  11964  sumtp  11965  fsum2dlemstep  11985  fsumiun  12028  isumlessdc  12047  zproddc  12130  fprodsplitdc  12147  fprodcl2lem  12156  fprod2dlemstep  12173  bezoutlemstep  12558  ennnfonelemim  13035  ctiunctal  13052  prdsmndd  13521  grppropd  13590  srgdilem  13972  srgrz  13987  srglz  13988  cnmpt11  14997  psmet0  15041  psmettri2  15042  mulcncflem  15321  mulcncf  15322  dedekindeulemuub  15331  dedekindeulemlu  15335  dedekindicclemuub  15340  dedekindicclemlu  15344  limccnpcntop  15389  limccnp2lem  15390  limccnp2cntop  15391  plycoeid3  15471  fsumdvdsmul  15705  bj-charfundc  16339  bj-charfunbi  16342  nninffeq  16558  refeq  16568  iswomni0  16591  nconstwlpolem  16605