Theorem 19.8ad 2220

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-12 2215

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

This theorem is used by:  2ax6e  2502  dfmoeu  2562  copsexgw  5470  copsexgwOLD  5471  domtriomlem  10448  axrepnd  10607  axunndlem1  10608  axunnd  10609  axpownd  10614  axacndlem1  10620  axacndlem2  10621  axacndlem3  10622  axacndlem4  10623  axacndlem5  10624  axacnd  10625  pwfseqlem4a  10674  pwfseqlem4  10675  bnj1189  35526  axtcond  37105  isbasisrelowllem1  38117  isbasisrelowllem2  38118  gneispace  44982  cpcolld  45090  ovncvrrp  47400  ichreuopeq  48381