Theorem 19.21bi 1537

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

Syntax hints:   → wi 4  ∀wal 1329

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

This theorem is referenced by:  19.21bbi  1538  ax11e  1768  eqeq1  2146  eleq2  2203  r19.21bi  2520  elrab3t  2839  ssel  3091  exmidsssn  4125  copsex2t  4167  pocl  4225  ordsucim  4416  peano2  4509  funmo  5138  funun  5167  fununi  5191  imain  5205  tfrlem3-2d  6209  tfr1onlemaccex  6245  tfri1dALT  6248  tfrcllemaccex  6258  findcard  6782  findcard2  6783  findcard2s  6784  exmidpw  6802