Theorem 19.21bi 2190

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

Syntax hints:   → wi 4  ∀wal 1540

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 1975  ax-7 2020  ax-12 2179

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

This theorem is referenced by:  19.21bbi  2191  axc7e  2320  eleq2w2  2734  eqeq1dALT  2741  eleq2dALT  2819  nfeqd  2909  sselOLD  3871  poclOLD  5450  funmo  6355  funun  6385  fununi  6414  findcard  8762  findcard2  8763  ssfi  8772  findcard2OLD  8834  axpowndlem4  10100  axregndlem2  10103  axinfnd  10106  prcdnq  10493  dfrtrcl2  14511  relexpindlem  14512  bnj1379  32381  bnj1052  32526  bnj1118  32535  bnj1154  32550  bnj1280  32571  dftrcl3  40874  dfrtrcl3  40887  vk15.4j  41686  hbimpg  41712