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 ⊢ (𝜑 → ∃𝑥𝜓)

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-12 2212

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

This theorem is used by:  2ax6e  2500  dfmoeu  2560  copsexgw  5459  copsexgwOLD  5460  cotsexgw  5462  domtriomlem  10523  axrepnd  10682  axunndlem1  10683  axunnd  10684  axpownd  10689  axacndlem1  10695  axacndlem2  10696  axacndlem3  10697  axacndlem4  10698  axacndlem5  10699  axacnd  10700  pwfseqlem4a  10749  pwfseqlem4  10750  bnj1189  35685  axtcond  37358  isbasisrelowllem1  38371  isbasisrelowllem2  38372  gneispace  45227  cpcolld  45335  ovncvrrp  47667  ichreuopeq  48648