Theorem 19.8ad 2218

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

Syntax hints:   → wi 4  ∃wex 1809

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-12 2213

This theorem depends on definitions:  df-bi 210  df-ex 1810

This theorem is referenced by:  2ax6e  2503  dfmoeu  2563  copsexgw  5474  copsexgwOLD  5475  domtriomlem  10427  axrepnd  10580  axunndlem1  10581  axunnd  10582  axpownd  10587  axacndlem1  10593  axacndlem2  10594  axacndlem3  10595  axacndlem4  10596  axacndlem5  10597  axacnd  10598  pwfseqlem4a  10647  pwfseqlem4  10648  bnj1189  35375  axtcond  36967  isbasisrelowllem1  37979  isbasisrelowllem2  37980  gneispace  44840  cpcolld  44948  ovncvrrp  47258  ichreuopeq  48199