Theorem 19.21bi 2201

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

Syntax hints:   → wi 4  ∀wal 1545

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-12 2189

This theorem depends on definitions:  df-bi 208  df-ex 1787

This theorem is referenced by:  19.21bbi  2202  axc7e  2327  eleq2w2  2735  eqeq1dALT  2742  eleq2dALT  2826  nfeqd  2911  funun  6531  fununi  6560  findcard  9088  findcard2  9089  ssfi  9097  ttrclselem2  9638  axpowndlem4  10514  axregndlem2  10517  axinfnd  10520  prcdnq  10907  dfrtrcl2  15015  relexpindlem  15016  bnj1379  35012  bnj1052  35157  bnj1118  35166  bnj1154  35181  bnj1280  35202  gblacfnacd  35330  onvf1odlem4  35334  mh-setind  36764  mh-setindnd  36765  dftrcl3  44164  dfrtrcl3  44177  vk15.4j  44972  hbimpg  44998  pgindnf  50206