Theorem 19.8ad 2175

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

Syntax hints:   → wi 4  ∃wex 1782

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-12 2171

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

This theorem is referenced by:  2ax6e  2471  dfmoeu  2536  copsexgw  5404  domtriomlem  10198  axrepnd  10350  axunndlem1  10351  axunnd  10352  axpownd  10357  axacndlem1  10363  axacndlem2  10364  axacndlem3  10365  axacndlem4  10366  axacndlem5  10367  axacnd  10368  pwfseqlem4a  10417  pwfseqlem4  10418  bnj1189  32989  isbasisrelowllem1  35526  isbasisrelowllem2  35527  gneispace  41744  cpcolld  41876  ovncvrrp  44102  ichreuopeq  44925