Theorem 19.21bi 1606

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

Syntax hints:   → wi 4  ∀wal 1395

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

This theorem is referenced by:  19.21bbi  1607  ax11e  1844  eqeq1  2238  eleq2  2295  r19.21bi  2620  elrab3t  2961  ssel  3221  exmidsssn  4292  copsex2t  4337  pocl  4400  ordsucim  4598  peano2  4693  funmo  5341  funun  5371  fununi  5398  imain  5412  tfrlem3-2d  6477  tfr1onlemaccex  6513  tfri1dALT  6516  tfrcllemaccex  6526  findcard  7076  findcard2  7077  findcard2s  7078  exmidpw  7099  exmidpweq  7100  nninfctlemfo  12610