![]() |
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 2955 | . 2 ⊢ (𝐴 ≠ 𝐵 → ¬ ¬ 𝜑) |
3 | 2 | notnotrd 133 | 1 ⊢ (𝐴 ≠ 𝐵 → 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 = wceq 1534 ≠ wne 2930 |
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 206 df-ne 2931 |
This theorem is referenced by: necon1i 2964 opnz 5471 inisegn0 6100 iotan0 6536 tz6.12i 6921 fvfundmfvn0 6936 brfvopabrbr 6998 elfvmptrab1 7029 brovpreldm 8095 brovex 8229 brwitnlem 8529 cantnflem1 9725 carddomi2 10006 rankcf 10811 1re 11255 eliooxr 13430 iccssioo2 13445 elfzoel1 13678 elfzoel2 13679 ismnd 18725 lactghmga 19399 pmtrmvd 19450 mpfrcl 22096 mhpsclcl 22137 fsubbas 23859 filuni 23877 ptcmplem2 24045 itg1climres 25732 mbfi1fseqlem4 25736 dvferm1lem 26004 dvferm2lem 26006 dvferm 26008 dvivthlem1 26029 coeeq2 26266 coe1termlem 26282 isppw 27139 dchrelbasd 27265 lgsne0 27361 wlkvv 29561 eldm3 35596 brfvimex 43730 brovmptimex 43731 clsneibex 43806 neicvgbex 43816 iotan0aiotaex 46742 afvnufveq 46796 gricrcl 47498 grlicrcl 47533 grilcbri2 47537 fvconstr 48259 fvconstrn0 48260 fvconstr2 48261 |
Copyright terms: Public domain | W3C validator |