![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > exlimi | Structured version Visualization version GIF version |
Description: Inference associated with 19.23 2227. See exlimiv 2007 for a version with a dv condition requiring fewer axioms. (Contributed by NM, 10-Jan-1993.) (Revised by Mario Carneiro, 24-Sep-2016.) |
Ref | Expression |
---|---|
exlimi.1 | ⊢ Ⅎ𝑥𝜓 |
exlimi.2 | ⊢ (𝜑 → 𝜓) |
Ref | Expression |
---|---|
exlimi | ⊢ (∃𝑥𝜑 → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | exlimi.1 | . . 3 ⊢ Ⅎ𝑥𝜓 | |
2 | 1 | 19.23 2227 | . 2 ⊢ (∀𝑥(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → 𝜓)) |
3 | exlimi.2 | . 2 ⊢ (𝜑 → 𝜓) | |
4 | 2, 3 | mpgbi 1874 | 1 ⊢ (∃𝑥𝜑 → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∃wex 1853 Ⅎwnf 1857 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1871 ax-4 1886 ax-5 1988 ax-6 2054 ax-7 2090 ax-12 2196 |
This theorem depends on definitions: df-bi 197 df-or 384 df-ex 1854 df-nf 1859 |
This theorem is referenced by: exlimih 2295 equs5aALT 2322 equs5eALT 2323 equsex 2437 nfeqf2 2442 exdistrf 2473 equs5a 2485 equs5e 2486 mo2v 2614 moanim 2667 euan 2668 moexex 2679 2eu6 2696 ceqsex 3381 sbhypf 3393 vtoclgf 3404 vtoclg1f 3405 vtoclef 3421 rspn0 4077 reusv2lem1 5017 copsexg 5104 copsex2g 5106 ralxpf 5424 dmcoss 5540 fv3 6367 tz6.12c 6374 opabiota 6423 0neqopab 6863 zfregcl 8664 scottex 8921 scott0 8922 dfac5lem5 9140 zfcndpow 9630 zfcndreg 9631 zfcndinf 9632 reclem2pr 10062 mreiincl 16458 brabgaf 29727 cnvoprabOLD 29807 bnj607 31293 bnj900 31306 exisym1 32729 exlimii 33124 bj-exlimmpi 33211 bj-exlimmpbi 33212 bj-exlimmpbir 33213 dihglblem5 37089 eu2ndop1stv 41708 |
Copyright terms: Public domain | W3C validator |