Theorem 19.21bi 2059

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

Syntax hints:   → wi 4  ∀wal 1481

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-12 2047

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

This theorem is referenced by:  19.21bbi  2060  eqeq1dALT  2625  eleq2dALT  2688  ssel  3597  pocl  5042  funmo  5904  funun  5932  fununi  5964  findcard  8199  findcard2  8200  axpowndlem4  9422  axregndlem2  9425  axinfnd  9428  prcdnq  9815  dfrtrcl2  13802  relexpindlem  13803  bnj1379  30901  bnj1052  31043  bnj1118  31052  bnj1154  31067  bnj1280  31088  dftrcl3  38012  dfrtrcl3  38025  vk15.4j  38734  hbimpg  38770