Theorem 19.21bi 1556

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

Syntax hints:   → wi 4  ∀wal 1351

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

This theorem is referenced by:  19.21bbi  1557  ax11e  1794  eqeq1  2182  eleq2  2239  r19.21bi  2563  elrab3t  2890  ssel  3147  exmidsssn  4197  copsex2t  4239  pocl  4297  ordsucim  4493  peano2  4588  funmo  5223  funun  5252  fununi  5276  imain  5290  tfrlem3-2d  6303  tfr1onlemaccex  6339  tfri1dALT  6342  tfrcllemaccex  6352  findcard  6878  findcard2  6879  findcard2s  6880  exmidpw  6898  exmidpweq  6899