Theorem 19.21bi 1607

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

Syntax hints:   → wi 4  ∀wal 1396

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

This theorem is referenced by:  19.21bbi  1608  ax11e  1844  eqeq1  2238  eleq2  2295  r19.21bi  2621  elrab3t  2962  ssel  3222  exmidsssn  4298  copsex2t  4343  pocl  4406  ordsucim  4604  peano2  4699  funmo  5348  funun  5378  fununi  5405  imain  5419  tfrlem3-2d  6521  tfr1onlemaccex  6557  tfri1dALT  6560  tfrcllemaccex  6570  findcard  7120  findcard2  7121  findcard2s  7122  exmidpw  7143  exmidpweq  7144  nninfctlemfo  12674