Theorem 19.8ad 2183

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

Syntax hints:   → wi 4  ∃wex 1777

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-12 2178

This theorem depends on definitions:  df-bi 207  df-ex 1778

This theorem is referenced by:  2ax6e  2479  dfmoeu  2539  copsexgw  5510  domtriomlem  10511  axrepnd  10663  axunndlem1  10664  axunnd  10665  axpownd  10670  axacndlem1  10676  axacndlem2  10677  axacndlem3  10678  axacndlem4  10679  axacndlem5  10680  axacnd  10681  pwfseqlem4a  10730  pwfseqlem4  10731  bnj1189  34985  isbasisrelowllem1  37321  isbasisrelowllem2  37322  gneispace  44096  cpcolld  44227  ovncvrrp  46485  ichreuopeq  47347