Theorem 19.21bi 1495

Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Contributed by NM, 5-Aug-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		ax-4 1445	. 2 ⊢ (∀𝑥𝜓 → 𝜓)
3	1, 2	syl 14	1 ⊢ (𝜑 → 𝜓)

Syntax hints:   → wi 4  ∀wal 1287

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-4 1445

This theorem is referenced by:  19.21bbi  1496  ax11e  1724  eqeq1  2094  eleq2  2151  r19.21bi  2461  elrab3t  2770  ssel  3019  copsex2t  4072  pocl  4130  ordsucim  4317  peano2  4410  funmo  5030  funun  5058  fununi  5082  imain  5096  tfrlem3-2d  6077  tfr1onlemaccex  6113  tfri1dALT  6116  tfrcllemaccex  6126  findcard  6602  findcard2  6603  findcard2s  6604  exmidpw  6622