Theorem 19.21bi 2213

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

Syntax hints:   → wi 4  ∀wal 1629

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-12 2203

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

This theorem is referenced by:  19.21bbi  2214  axc7e  2297  eqeq1dALT  2774  eleq2dALT  2837  ssel  3746  pocl  5177  funmo  6047  funun  6075  fununi  6104  findcard  8355  findcard2  8356  axpowndlem4  9624  axregndlem2  9627  axinfnd  9630  prcdnq  10017  dfrtrcl2  14010  relexpindlem  14011  bnj1379  31239  bnj1052  31381  bnj1118  31390  bnj1154  31405  bnj1280  31426  dftrcl3  38538  dfrtrcl3  38551  vk15.4j  39259  hbimpg  39295