Theorem 19.8ad 2179

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

Syntax hints:   → wi 4  ∃wex 1786

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-12 2175

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

This theorem is referenced by:  2ax6e  2473  dfmoeu  2538  copsexgw  5408  domtriomlem  10199  axrepnd  10351  axunndlem1  10352  axunnd  10353  axpownd  10358  axacndlem1  10364  axacndlem2  10365  axacndlem3  10366  axacndlem4  10367  axacndlem5  10368  axacnd  10369  pwfseqlem4a  10418  pwfseqlem4  10419  bnj1189  32985  isbasisrelowllem1  35522  isbasisrelowllem2  35523  gneispace  41714  cpcolld  41846  ovncvrrp  44073  ichreuopeq  44894