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  4286  copsex2t  4331  pocl  4394  ordsucim  4592  peano2  4687  funmo  5333  funun  5362  fununi  5389  imain  5403  tfrlem3-2d  6464  tfr1onlemaccex  6500  tfri1dALT  6503  tfrcllemaccex  6513  findcard  7058  findcard2  7059  findcard2s  7060  exmidpw  7081  exmidpweq  7082  nninfctlemfo  12576