Theorem 19.8ad 2190

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

Syntax hints:   → wi 4  ∃wex 1781

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-12 2185

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

This theorem is referenced by:  2ax6e  2476  dfmoeu  2536  copsexgw  5438  domtriomlem  10355  axrepnd  10508  axunndlem1  10509  axunnd  10510  axpownd  10515  axacndlem1  10521  axacndlem2  10522  axacndlem3  10523  axacndlem4  10524  axacndlem5  10525  axacnd  10526  pwfseqlem4a  10575  pwfseqlem4  10576  bnj1189  35167  axtcond  36676  isbasisrelowllem1  37685  isbasisrelowllem2  37686  gneispace  44579  cpcolld  44703  ovncvrrp  47010  ichreuopeq  47945