Theorem 19.21bi 1572

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 1524	. 2 ⊢ (∀𝑥𝜓 → 𝜓)
3	1, 2	syl 14	1 ⊢ (𝜑 → 𝜓)

Syntax hints:   → wi 4  ∀wal 1362

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

This theorem is referenced by:  19.21bbi  1573  ax11e  1810  eqeq1  2203  eleq2  2260  r19.21bi  2585  elrab3t  2919  ssel  3177  exmidsssn  4235  copsex2t  4278  pocl  4338  ordsucim  4536  peano2  4631  funmo  5273  funun  5302  fununi  5326  imain  5340  tfrlem3-2d  6370  tfr1onlemaccex  6406  tfri1dALT  6409  tfrcllemaccex  6419  findcard  6949  findcard2  6950  findcard2s  6951  exmidpw  6969  exmidpweq  6970  nninfctlemfo  12207