Theorem 19.21bi 2194

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

Syntax hints:   → wi 4  ∀wal 1539

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 1968  ax-7 2009  ax-12 2182

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

This theorem is referenced by:  19.21bbi  2195  axc7e  2321  eleq2w2  2729  eqeq1dALT  2736  eleq2dALT  2820  nfeqd  2906  funun  6535  fununi  6564  findcard  9084  findcard2  9085  ssfi  9093  ttrclselem2  9627  axpowndlem4  10502  axregndlem2  10505  axinfnd  10508  prcdnq  10895  dfrtrcl2  14976  relexpindlem  14977  bnj1379  34914  bnj1052  35059  bnj1118  35068  bnj1154  35083  bnj1280  35104  gblacfnacd  35218  onvf1odlem4  35222  dftrcl3  43877  dfrtrcl3  43890  vk15.4j  44685  hbimpg  44711  pgindnf  49877