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  5427  domtriomlem  10324  axrepnd  10476  axunndlem1  10477  axunnd  10478  axpownd  10483  axacndlem1  10489  axacndlem2  10490  axacndlem3  10491  axacndlem4  10492  axacndlem5  10493  axacnd  10494  pwfseqlem4a  10543  pwfseqlem4  10544  bnj1189  34989  isbasisrelowllem1  37346  isbasisrelowllem2  37347  gneispace  44124  cpcolld  44248  ovncvrrp  46559  ichreuopeq  47471