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  2958  ssel  3218  exmidsssn  4285  copsex2t  4330  pocl  4393  ordsucim  4591  peano2  4686  funmo  5332  funun  5361  fununi  5388  imain  5402  tfrlem3-2d  6456  tfr1onlemaccex  6492  tfri1dALT  6495  tfrcllemaccex  6505  findcard  7046  findcard2  7047  findcard2s  7048  exmidpw  7066  exmidpweq  7067  nninfctlemfo  12556