Theorem 19.21bi 2189

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

Syntax hints:   → wi 4  ∀wal 1538

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-12 2177

This theorem depends on definitions:  df-bi 207  df-ex 1780

This theorem is referenced by:  19.21bbi  2190  axc7e  2318  eleq2w2  2733  eqeq1dALT  2740  eleq2dALT  2828  nfeqd  2916  funmoOLD  6582  funun  6612  fununi  6641  findcard  9203  findcard2  9204  ssfi  9213  ttrclselem2  9766  axpowndlem4  10640  axregndlem2  10643  axinfnd  10646  prcdnq  11033  dfrtrcl2  15101  relexpindlem  15102  bnj1379  34844  bnj1052  34989  bnj1118  34998  bnj1154  35013  bnj1280  35034  gblacfnacd  35113  dftrcl3  43733  dfrtrcl3  43746  vk15.4j  44548  hbimpg  44574  pgindnf  49235