Theorem 19.8ad 2189

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

Syntax hints:   → wi 4  ∃wex 1780

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-12 2184

This theorem depends on definitions:  df-bi 207  df-ex 1781

This theorem is referenced by:  2ax6e  2475  dfmoeu  2535  copsexgw  5438  domtriomlem  10352  axrepnd  10505  axunndlem1  10506  axunnd  10507  axpownd  10512  axacndlem1  10518  axacndlem2  10519  axacndlem3  10520  axacndlem4  10521  axacndlem5  10522  axacnd  10523  pwfseqlem4a  10572  pwfseqlem4  10573  bnj1189  35165  isbasisrelowllem1  37560  isbasisrelowllem2  37561  gneispace  44375  cpcolld  44499  ovncvrrp  46808  ichreuopeq  47719