Theorem 19.8ad 2220

Description: If a wff is true, it is true for at least one instance. Deduction form of 19.8a 2219. (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 2219	. 2 ⊢ (𝜓 → ∃𝑥𝜓)
3	1, 2	syl 18	1 ⊢ (𝜑 → ∃𝑥𝜓)

Syntax hints:   → wi 4  ∃wex 1802

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-12 2215

This theorem depends on definitions:  df-bi 210  df-ex 1803

This theorem is referenced by:  2ax6e  2505  dfmoeu  2565  copsexgw  5463  copsexgwOLD  5464  domtriomlem  10414  axrepnd  10567  axunndlem1  10568  axunnd  10569  axpownd  10574  axacndlem1  10580  axacndlem2  10581  axacndlem3  10582  axacndlem4  10583  axacndlem5  10584  axacnd  10585  pwfseqlem4a  10634  pwfseqlem4  10635  bnj1189  35314  axtcond  36851  isbasisrelowllem1  37861  isbasisrelowllem2  37862  gneispace  44722  cpcolld  44832  ovncvrrp  47136  ichreuopeq  48077