Theorem 19.8ad 2176

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

Syntax hints:   → wi 4  ∃wex 1782

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-12 2172

This theorem depends on definitions:  df-bi 206  df-ex 1783

This theorem is referenced by:  2ax6e  2471  dfmoeu  2531  copsexgw  5491  domtriomlem  10437  axrepnd  10589  axunndlem1  10590  axunnd  10591  axpownd  10596  axacndlem1  10602  axacndlem2  10603  axacndlem3  10604  axacndlem4  10605  axacndlem5  10606  axacnd  10607  pwfseqlem4a  10656  pwfseqlem4  10657  bnj1189  34051  isbasisrelowllem1  36284  isbasisrelowllem2  36285  gneispace  42933  cpcolld  43065  ovncvrrp  45328  ichreuopeq  46189