Theorem 19.8ad 2185

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

Syntax hints:   → wi 4  ∃wex 1780

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-12 2180

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

This theorem is referenced by:  2ax6e  2471  dfmoeu  2531  copsexgw  5430  domtriomlem  10333  axrepnd  10485  axunndlem1  10486  axunnd  10487  axpownd  10492  axacndlem1  10498  axacndlem2  10499  axacndlem3  10500  axacndlem4  10501  axacndlem5  10502  axacnd  10503  pwfseqlem4a  10552  pwfseqlem4  10553  bnj1189  35019  isbasisrelowllem1  37395  isbasisrelowllem2  37396  gneispace  44173  cpcolld  44297  ovncvrrp  46608  ichreuopeq  47510