Theorem 19.8ad 2180

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

Syntax hints:   → wi 4  ∃wex 1776

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-12 2175

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

This theorem is referenced by:  2ax6e  2474  dfmoeu  2534  copsexgw  5501  domtriomlem  10480  axrepnd  10632  axunndlem1  10633  axunnd  10634  axpownd  10639  axacndlem1  10645  axacndlem2  10646  axacndlem3  10647  axacndlem4  10648  axacndlem5  10649  axacnd  10650  pwfseqlem4a  10699  pwfseqlem4  10700  bnj1189  35002  isbasisrelowllem1  37338  isbasisrelowllem2  37339  gneispace  44124  cpcolld  44254  ovncvrrp  46520  ichreuopeq  47398