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  6478  tfr1onlemaccex  6514  tfri1dALT  6517  tfrcllemaccex  6527  findcard  7077  findcard2  7078  findcard2s  7079  exmidpw  7100  exmidpweq  7101  nninfctlemfo  12616