Theorem 19.8ad 2217

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

This proof depends on syntax axioms:   → wi 4  ∃wex 1808

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-12 2212

This proof depends on definitions:  df-bi 210  df-ex 1809

This theorem is used by:  2ax6e  2502  dfmoeu  2562  copsexgw  5471  copsexgwOLD  5472  domtriomlem  10432  axrepnd  10585  axunndlem1  10586  axunnd  10587  axpownd  10592  axacndlem1  10598  axacndlem2  10599  axacndlem3  10600  axacndlem4  10601  axacndlem5  10602  axacnd  10603  pwfseqlem4a  10652  pwfseqlem4  10653  bnj1189  35406  axtcond  37017  isbasisrelowllem1  38029  isbasisrelowllem2  38030  gneispace  44888  cpcolld  44996  ovncvrrp  47306  ichreuopeq  48250