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  5450  domtriomlem  10395  axrepnd  10547  axunndlem1  10548  axunnd  10549  axpownd  10554  axacndlem1  10560  axacndlem2  10561  axacndlem3  10562  axacndlem4  10563  axacndlem5  10564  axacnd  10565  pwfseqlem4a  10614  pwfseqlem4  10615  bnj1189  34999  isbasisrelowllem1  37343  isbasisrelowllem2  37344  gneispace  44123  cpcolld  44247  ovncvrrp  46562  ichreuopeq  47471