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 2170. (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 2170 | . 2 ⊢ (𝜓 → ∃𝑥𝜓) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → ∃𝑥𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∃wex 1771 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-12 2167 |
This theorem depends on definitions: df-bi 208 df-ex 1772 |
This theorem is referenced by: 2ax6e 2486 dfmoeu 2611 copsexgw 5372 domtriomlem 9852 axrepnd 10004 axunndlem1 10005 axunnd 10006 axpownd 10011 axacndlem1 10017 axacndlem2 10018 axacndlem3 10019 axacndlem4 10020 axacndlem5 10021 axacnd 10022 pwfseqlem4a 10071 pwfseqlem4 10072 bnj1189 32178 isbasisrelowllem1 34518 isbasisrelowllem2 34519 gneispace 40362 cpcolld 40471 ovncvrrp 42723 ichreuopeq 43512 |
Copyright terms: Public domain | W3C validator |