Theorem 19.8ad 2216

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

Syntax hints:   → wi 4  ∃wex 1798

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-12 2211

This theorem depends on definitions:  df-bi 209  df-ex 1799

This theorem is referenced by:  2ax6e  2501  dfmoeu  2561  copsexgw  5457  copsexgwOLD  5458  domtriomlem  10396  axrepnd  10549  axunndlem1  10550  axunnd  10551  axpownd  10556  axacndlem1  10562  axacndlem2  10563  axacndlem3  10564  axacndlem4  10565  axacndlem5  10566  axacnd  10567  pwfseqlem4a  10616  pwfseqlem4  10617  bnj1189  35268  axtcond  36802  isbasisrelowllem1  37813  isbasisrelowllem2  37814  gneispace  44674  cpcolld  44798  ovncvrrp  47102  ichreuopeq  48043