Theorem 19.21bi 2173

Description: Inference form of 19.21 2192 and also deduction form of sp 2167. (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 2167	. 2 ⊢ (∀𝑥𝜓 → 𝜓)
3	1, 2	syl 17	1 ⊢ (𝜑 → 𝜓)

Syntax hints:   → wi 4  ∀wal 1599

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-12 2163

This theorem depends on definitions:  df-bi 199  df-ex 1824

This theorem is referenced by:  19.21bbi  2174  axc7e  2293  eqeq1dALT  2781  eleq2dALT  2846  ssel  3815  pocl  5281  funmo  6151  funun  6180  fununi  6209  findcard  8487  findcard2  8488  axpowndlem4  9757  axregndlem2  9760  axinfnd  9763  prcdnq  10150  dfrtrcl2  14209  relexpindlem  14210  bnj1379  31500  bnj1052  31642  bnj1118  31651  bnj1154  31666  bnj1280  31687  dftrcl3  38969  dfrtrcl3  38982  vk15.4j  39688  hbimpg  39714