Theorem 19.8ad 2222

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

This proof depends on syntax axioms:   → wi 4  ∃wex 1812

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-12 2216

This proof depends on definitions:  df-bi 210  df-ex 1813

This theorem is used by:  2ax6e  2503  dfmoeu  2563  copsexgw  5464  copsexgwOLD  5465  cotsexgw  5467  domtriomlem  10547  axrepnd  10706  axunndlem1  10707  axunnd  10708  axpownd  10713  axacndlem1  10719  axacndlem2  10720  axacndlem3  10721  axacndlem4  10722  axacndlem5  10723  axacnd  10724  pwfseqlem4a  10773  pwfseqlem4  10774  bnj1189  35709  axtcond  37444  isbasisrelowllem1  38470  isbasisrelowllem2  38471  gneispace  45326  cpcolld  45434  ovncvrrp  47779  ichreuopeq  48760