Theorem 19.21bi 2224

Description: Inference form of 19.21 2242 and also deduction form of sp 2218. (Contributed by NM, 26-May-1993.)

Hypothesis

Ref	Expression
19.21bi.1	⊢ (𝜑 → ∀𝑥𝜓)

Assertion

Ref	Expression
19.21bi	⊢ (𝜑 → 𝜓)

Proof of Theorem 19.21bi

Step	Hyp	Ref	Expression
1		19.21bi.1	. 2 ⊢ (𝜑 → ∀𝑥𝜓)
2		sp 2218	. 2 ⊢ (∀𝑥𝜓 → 𝜓)
3	1, 2	syl 17	1 ⊢ (𝜑 → 𝜓)

Syntax hints:   → wi 4  ∀wal 1558

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-12 2212

This theorem depends on definitions:  df-bi 209  df-ex 1800

This theorem is referenced by:  19.21bbi  2225  axc7e  2350  eleq2w2  2758  eqeq1dALT  2765  eleq2dALT  2849  nfeqd  2934  funun  6567  fununi  6596  findcard  9132  findcard2  9133  ssfi  9141  ttrclselem2  9681  axpowndlem4  10558  axregndlem2  10561  axinfnd  10564  prcdnq  10951  dfrtrcl2  15075  relexpindlem  15076  bnj1379  35122  bnj1052  35267  bnj1118  35276  bnj1154  35291  bnj1280  35312  gblacfnacd  35442  onvf1odlem4  35446  mh-setind  36893  mh-setindnd  36894  dftrcl3  44293  dfrtrcl3  44306  vk15.4j  45101  hbimpg  45127  pgindnf  50334