Theorem 19.8ad 2177

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

Syntax hints:   → wi 4  ∃wex 1783

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-12 2173

This theorem depends on definitions:  df-bi 206  df-ex 1784

This theorem is referenced by:  2ax6e  2471  dfmoeu  2536  copsexgw  5398  domtriomlem  10129  axrepnd  10281  axunndlem1  10282  axunnd  10283  axpownd  10288  axacndlem1  10294  axacndlem2  10295  axacndlem3  10296  axacndlem4  10297  axacndlem5  10298  axacnd  10299  pwfseqlem4a  10348  pwfseqlem4  10349  bnj1189  32889  isbasisrelowllem1  35453  isbasisrelowllem2  35454  gneispace  41633  cpcolld  41765  ovncvrrp  43992  ichreuopeq  44813