Theorem 19.21bi 1580

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

Syntax hints:   → wi 4  ∀wal 1370

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

This theorem is referenced by:  19.21bbi  1581  ax11e  1818  eqeq1  2211  eleq2  2268  r19.21bi  2593  elrab3t  2927  ssel  3186  exmidsssn  4245  copsex2t  4288  pocl  4349  ordsucim  4547  peano2  4642  funmo  5285  funun  5314  fununi  5341  imain  5355  tfrlem3-2d  6397  tfr1onlemaccex  6433  tfri1dALT  6436  tfrcllemaccex  6446  findcard  6984  findcard2  6985  findcard2s  6986  exmidpw  7004  exmidpweq  7005  nninfctlemfo  12303