Theorem 19.8ad 2190

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

Syntax hints:   → wi 4  ∃wex 1781

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-12 2185

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

This theorem is referenced by:  2ax6e  2476  dfmoeu  2536  copsexgw  5446  domtriomlem  10364  axrepnd  10517  axunndlem1  10518  axunnd  10519  axpownd  10524  axacndlem1  10530  axacndlem2  10531  axacndlem3  10532  axacndlem4  10533  axacndlem5  10534  axacnd  10535  pwfseqlem4a  10584  pwfseqlem4  10585  bnj1189  35184  isbasisrelowllem1  37607  isbasisrelowllem2  37608  gneispace  44487  cpcolld  44611  ovncvrrp  46919  ichreuopeq  47830