Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > necon1ai | Structured version Visualization version GIF version |
Description: Contrapositive inference for inequality. (Contributed by NM, 12-Feb-2007.) (Proof shortened by Wolf Lammen, 22-Nov-2019.) |
Ref | Expression |
---|---|
necon1ai.1 | ⊢ (¬ 𝜑 → 𝐴 = 𝐵) |
Ref | Expression |
---|---|
necon1ai | ⊢ (𝐴 ≠ 𝐵 → 𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | necon1ai.1 | . . 3 ⊢ (¬ 𝜑 → 𝐴 = 𝐵) | |
2 | 1 | necon3ai 3041 | . 2 ⊢ (𝐴 ≠ 𝐵 → ¬ ¬ 𝜑) |
3 | 2 | notnotrd 135 | 1 ⊢ (𝐴 ≠ 𝐵 → 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 = wceq 1528 ≠ wne 3016 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 208 df-ne 3017 |
This theorem is referenced by: necon1i 3049 opnz 5357 inisegn0 5955 iotan0 6339 tz6.12i 6690 fvfundmfvn0 6702 brfvopabrbr 6759 elfvmptrab1 6788 brovpreldm 7775 brovex 7879 brwitnlem 8123 cantnflem1 9141 carddomi2 9388 rankcf 10188 1re 10630 eliooxr 12785 iccssioo2 12799 elfzoel1 13026 elfzoel2 13027 ismnd 17904 lactghmga 18464 pmtrmvd 18515 mpfrcl 20228 fsubbas 22405 filuni 22423 ptcmplem2 22591 itg1climres 24244 mbfi1fseqlem4 24248 dvferm1lem 24510 dvferm2lem 24512 dvferm 24514 dvivthlem1 24534 coeeq2 24761 coe1termlem 24777 isppw 25619 dchrelbasd 25743 lgsne0 25839 wlkvv 27336 eldm3 32895 brfvimex 40256 brovmptimex 40257 clsneibex 40332 neicvgbex 40342 iotan0aiotaex 43172 afvnufveq 43227 |
Copyright terms: Public domain | W3C validator |