Theorem 19.8ad 2221

Description: If a wff is true, it is true for at least one instance. Deduction form of 19.8a 2220. (Contributed by DAW, 13-Feb-2017.)

Hypothesis

Ref	Expression
19.8ad.1	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
19.8ad	⊢ (𝜑 → ∃𝑥𝜓)

Proof of Theorem 19.8ad

Step	Hyp	Ref	Expression
1		19.8ad.1	. 2 ⊢ (𝜑 → 𝜓)
2		19.8a 2220	. 2 ⊢ (𝜓 → ∃𝑥𝜓)
3	1, 2	syl 18	1 ⊢ (𝜑 → ∃𝑥𝜓)

This proof depends on syntax axioms:   → wi 4  ∃wex 1812

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-12 2216

This proof depends on definitions:  df-bi 210  df-ex 1813

This theorem is used by:  2ax6e  2506  dfmoeu  2566  copsexgw  5477  copsexgwOLD  5478  domtriomlem  10444  axrepnd  10597  axunndlem1  10598  axunnd  10599  axpownd  10604  axacndlem1  10610  axacndlem2  10611  axacndlem3  10612  axacndlem4  10613  axacndlem5  10614  axacnd  10615  pwfseqlem4a  10664  pwfseqlem4  10665  bnj1189  35429  axtcond  37030  isbasisrelowllem1  38042  isbasisrelowllem2  38043  gneispace  44901  cpcolld  45009  ovncvrrp  47319  ichreuopeq  48263