Theorem 19.8ad 2179

Description: If a wff is true, it is true for at least one instance. Deduction form of 19.8a 2178. (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 2178	. 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 1911  ax-6 1970  ax-7 2015  ax-12 2175

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

This theorem is referenced by:  2ax6e  2483  dfmoeu  2594  copsexgw  5346  domtriomlem  9853  axrepnd  10005  axunndlem1  10006  axunnd  10007  axpownd  10012  axacndlem1  10018  axacndlem2  10019  axacndlem3  10020  axacndlem4  10021  axacndlem5  10022  axacnd  10023  pwfseqlem4a  10072  pwfseqlem4  10073  bnj1189  32391  isbasisrelowllem1  34772  isbasisrelowllem2  34773  gneispace  40837  cpcolld  40966  ovncvrrp  43203  ichreuopeq  43990