Theorem 19.21bi 2057

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

Syntax hints:   → wi 4  ∀wal 1479

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-12 2045

This theorem depends on definitions:  df-bi 197  df-ex 1703

This theorem is referenced by:  19.21bbi  2058  eqeq1dALT  2623  eleq2dALT  2686  ssel  3589  pocl  5032  funmo  5892  funun  5920  fununi  5952  findcard  8184  findcard2  8185  axpowndlem4  9407  axregndlem2  9410  axinfnd  9413  prcdnq  9800  dfrtrcl2  13783  relexpindlem  13784  bnj1379  30875  bnj1052  31017  bnj1118  31026  bnj1154  31041  bnj1280  31062  dftrcl3  37831  dfrtrcl3  37844  vk15.4j  38554  hbimpg  38590