Theorem 19.21bi 1582

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

Syntax hints:   → wi 4  ∀wal 1371

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

This theorem is referenced by:  19.21bbi  1583  ax11e  1820  eqeq1  2213  eleq2  2270  r19.21bi  2595  elrab3t  2932  ssel  3191  exmidsssn  4254  copsex2t  4297  pocl  4358  ordsucim  4556  peano2  4651  funmo  5295  funun  5324  fununi  5351  imain  5365  tfrlem3-2d  6411  tfr1onlemaccex  6447  tfri1dALT  6450  tfrcllemaccex  6460  findcard  7000  findcard2  7001  findcard2s  7002  exmidpw  7020  exmidpweq  7021  nninfctlemfo  12436