Theorem 19.21bi 1604

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

Syntax hints:   → wi 4  ∀wal 1393

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

This theorem is referenced by:  19.21bbi  1605  ax11e  1842  eqeq1  2236  eleq2  2293  r19.21bi  2618  elrab3t  2959  ssel  3219  exmidsssn  4290  copsex2t  4335  pocl  4398  ordsucim  4596  peano2  4691  funmo  5339  funun  5368  fununi  5395  imain  5409  tfrlem3-2d  6473  tfr1onlemaccex  6509  tfri1dALT  6512  tfrcllemaccex  6522  findcard  7070  findcard2  7071  findcard2s  7072  exmidpw  7093  exmidpweq  7094  nninfctlemfo  12601