Theorem 19.8ad 2194

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

Syntax hints:   → wi 4  ∃wex 1786

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-12 2189

This theorem depends on definitions:  df-bi 208  df-ex 1787

This theorem is referenced by:  2ax6e  2479  dfmoeu  2539  copsexgw  5437  copsexgwOLD  5438  domtriomlem  10362  axrepnd  10515  axunndlem1  10516  axunnd  10517  axpownd  10522  axacndlem1  10528  axacndlem2  10529  axacndlem3  10530  axacndlem4  10531  axacndlem5  10532  axacnd  10533  pwfseqlem4a  10582  pwfseqlem4  10583  bnj1189  35198  axtcond  36713  isbasisrelowllem1  37724  isbasisrelowllem2  37725  gneispace  44585  cpcolld  44709  ovncvrrp  47014  ichreuopeq  47955