Theorem 19.8ad 2181

Description: If a wff is true, it is true for at least one instance. Deduction form of 19.8a 2180. (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 2180	. 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 1970  ax-7 2015  ax-12 2177

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

This theorem is referenced by:  2ax6e  2494  dfmoeu  2618  copsexgw  5381  domtriomlem  9864  axrepnd  10016  axunndlem1  10017  axunnd  10018  axpownd  10023  axacndlem1  10029  axacndlem2  10030  axacndlem3  10031  axacndlem4  10032  axacndlem5  10033  axacnd  10034  pwfseqlem4a  10083  pwfseqlem4  10084  bnj1189  32281  isbasisrelowllem1  34639  isbasisrelowllem2  34640  gneispace  40504  cpcolld  40614  ovncvrrp  42866  ichreuopeq  43655