Theorem 19.21bi 2188

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

Syntax hints:   → wi 4  ∀wal 1535

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-12 2177

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

This theorem is referenced by:  19.21bbi  2189  axc7e  2337  eqeq1dALT  2826  eleq2dALT  2901  ssel  3963  pocl  5483  funmo  6373  funun  6402  fununi  6431  findcard  8759  findcard2  8760  axpowndlem4  10024  axregndlem2  10027  axinfnd  10030  prcdnq  10417  dfrtrcl2  14423  relexpindlem  14424  bnj1379  32104  bnj1052  32249  bnj1118  32258  bnj1154  32273  bnj1280  32294  dftrcl3  40072  dfrtrcl3  40085  vk15.4j  40869  hbimpg  40895