Theorem 19.8ad 2170

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

Syntax hints:   → wi 4  ∃wex 1773

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-12 2166

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

This theorem is referenced by:  2ax6e  2464  dfmoeu  2524  copsexgw  5492  domtriomlem  10467  axrepnd  10619  axunndlem1  10620  axunnd  10621  axpownd  10626  axacndlem1  10632  axacndlem2  10633  axacndlem3  10634  axacndlem4  10635  axacndlem5  10636  axacnd  10637  pwfseqlem4a  10686  pwfseqlem4  10687  bnj1189  34768  isbasisrelowllem1  36962  isbasisrelowllem2  36963  gneispace  43703  cpcolld  43834  ovncvrrp  46087  ichreuopeq  46947