19.8ad - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > 19.8ad		Structured version Visualization version GIF version

Theorem 19.8ad 2171

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

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∃wex 1774

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-12 2167

This theorem depends on definitions: df-bi 206 df-ex 1775

This theorem is referenced by: 2ax6e 2466 dfmoeu 2526 copsexgw 5492 domtriomlem 10465 axrepnd 10617 axunndlem1 10618 axunnd 10619 axpownd 10624 axacndlem1 10630 axacndlem2 10631 axacndlem3 10632 axacndlem4 10633 axacndlem5 10634 axacnd 10635 pwfseqlem4a 10684 pwfseqlem4 10685 bnj1189 34640 isbasisrelowllem1 36834 isbasisrelowllem2 36835 gneispace 43564 cpcolld 43695 ovncvrrp 45952 ichreuopeq 46813

	
		OSZAR »