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  4348  ordsucim  4546  peano2  4641  funmo  5283  funun  5312  fununi  5336  imain  5350  tfrlem3-2d  6388  tfr1onlemaccex  6424  tfri1dALT  6427  tfrcllemaccex  6437  findcard  6967  findcard2  6968  findcard2s  6969  exmidpw  6987  exmidpweq  6988  nninfctlemfo  12280