Theorem 19.8ad 2219

Description: If a wff is true, it is true for at least one instance. Deduction form of 19.8a 2218. (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 2218	. 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 2213

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

This theorem is used by:  2ax6e  2501  dfmoeu  2561  copsexgw  5460  copsexgwOLD  5461  cotsexgw  5463  domtriomlem  10501  axrepnd  10660  axunndlem1  10661  axunnd  10662  axpownd  10667  axacndlem1  10673  axacndlem2  10674  axacndlem3  10675  axacndlem4  10676  axacndlem5  10677  axacnd  10678  pwfseqlem4a  10727  pwfseqlem4  10728  bnj1189  35622  axtcond  37236  isbasisrelowllem1  38246  isbasisrelowllem2  38247  gneispace  45093  cpcolld  45201  ovncvrrp  47518  ichreuopeq  48499