Theorem 19.8ad 2183

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

Syntax hints:   → wi 4  ∃wex 1779

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-12 2178

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

This theorem is referenced by:  2ax6e  2469  dfmoeu  2529  copsexgw  5437  domtriomlem  10355  axrepnd  10507  axunndlem1  10508  axunnd  10509  axpownd  10514  axacndlem1  10520  axacndlem2  10521  axacndlem3  10522  axacndlem4  10523  axacndlem5  10524  axacnd  10525  pwfseqlem4a  10574  pwfseqlem4  10575  bnj1189  34978  isbasisrelowllem1  37331  isbasisrelowllem2  37332  gneispace  44110  cpcolld  44234  ovncvrrp  46549  ichreuopeq  47461