Theorem 19.8ad 2187

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

Syntax hints:   → wi 4  ∃wex 1780

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-12 2182

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

This theorem is referenced by:  2ax6e  2473  dfmoeu  2533  copsexgw  5433  domtriomlem  10340  axrepnd  10492  axunndlem1  10493  axunnd  10494  axpownd  10499  axacndlem1  10505  axacndlem2  10506  axacndlem3  10507  axacndlem4  10508  axacndlem5  10509  axacnd  10510  pwfseqlem4a  10559  pwfseqlem4  10560  bnj1189  35042  isbasisrelowllem1  37420  isbasisrelowllem2  37421  gneispace  44252  cpcolld  44376  ovncvrrp  46687  ichreuopeq  47598