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 1779

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-12 2178

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

This theorem is referenced by:  2ax6e  2476  dfmoeu  2536  copsexgw  5470  domtriomlem  10461  axrepnd  10613  axunndlem1  10614  axunnd  10615  axpownd  10620  axacndlem1  10626  axacndlem2  10627  axacndlem3  10628  axacndlem4  10629  axacndlem5  10630  axacnd  10631  pwfseqlem4a  10680  pwfseqlem4  10681  bnj1189  35045  isbasisrelowllem1  37378  isbasisrelowllem2  37379  gneispace  44125  cpcolld  44249  ovncvrrp  46560  ichreuopeq  47454