Theorem 19.21bi 1607

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

Syntax hints:   → wi 4  ∀wal 1396

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

This theorem is referenced by:  19.21bbi  1608  ax11e  1845  eqeq1  2239  eleq2  2296  r19.21bi  2630  elrab3t  2972  ssel  3232  exmidsssn  4315  copsex2t  4361  pocl  4424  ordsucim  4622  peano2  4717  funmo  5367  funun  5397  fununi  5424  imain  5438  tfrlem3-2d  6543  tfr1onlemaccex  6579  tfri1dALT  6582  tfrcllemaccex  6592  findcard  7145  findcard2  7146  findcard2s  7147  exmidpw  7168  exmidpweq  7169  nninfctlemfo  12736