![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 19.8ad | Structured version Visualization version GIF version |
Description: If a wff is true, it is true for at least one instance. Deduction form of 19.8a 2169. (Contributed by DAW, 13-Feb-2017.) |
Ref | Expression |
---|---|
19.8ad.1 | ⊢ (𝜑 → 𝜓) |
Ref | Expression |
---|---|
19.8ad | ⊢ (𝜑 → ∃𝑥𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 19.8ad.1 | . 2 ⊢ (𝜑 → 𝜓) | |
2 | 19.8a 2169 | . 2 ⊢ (𝜓 → ∃𝑥𝜓) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → ∃𝑥𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∃wex 1773 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-12 2166 |
This theorem depends on definitions: df-bi 206 df-ex 1774 |
This theorem is referenced by: 2ax6e 2464 dfmoeu 2524 copsexgw 5492 domtriomlem 10467 axrepnd 10619 axunndlem1 10620 axunnd 10621 axpownd 10626 axacndlem1 10632 axacndlem2 10633 axacndlem3 10634 axacndlem4 10635 axacndlem5 10636 axacnd 10637 pwfseqlem4a 10686 pwfseqlem4 10687 bnj1189 34768 isbasisrelowllem1 36962 isbasisrelowllem2 36963 gneispace 43703 cpcolld 43834 ovncvrrp 46087 ichreuopeq 46947 |
Copyright terms: Public domain | W3C validator |