Theorem 19.21bi 1611

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

This proof depends on syntax axioms:   → wi 4  ∀wal 1400

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-4 1563

This theorem is used by:  19.21bbi  1612  ax11e  1849  eqeq1  2245  eleq2  2302  r19.21bi  2638  elrab3t  2981  ssel  3242  exmidsssn  4341  copsex2t  4387  pocl  4450  ordsucim  4649  peano2  4744  funmo  5395  funun  5425  fununi  5452  imain  5466  tfrlem3-2d  6587  tfr1onlemaccex  6623  tfri1dALT  6626  tfrcllemaccex  6636  findcard  7196  findcard2  7197  findcard2s  7198  exmidpw  7219  exmidpweq  7220  nninfctlemfo  12842