|   | 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 2964 | . 2 ⊢ (𝐴 ≠ 𝐵 → ¬ ¬ 𝜑) | 
| 3 | 2 | notnotrd 133 | 1 ⊢ (𝐴 ≠ 𝐵 → 𝜑) | 
| Colors of variables: wff setvar class | 
| Syntax hints: ¬ wn 3 → wi 4 = wceq 1539 ≠ wne 2939 | 
| 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 207 df-ne 2940 | 
| This theorem is referenced by: necon1i 2973 opnz 5477 inisegn0 6115 iotan0 6550 tz6.12i 6933 fvfundmfvn0 6948 brfvopabrbr 7012 elfvmptrab1 7043 brovpreldm 8115 brovex 8248 brwitnlem 8546 cantnflem1 9730 carddomi2 10011 rankcf 10818 1re 11262 eliooxr 13446 iccssioo2 13461 elfzoel1 13698 elfzoel2 13699 ismnd 18751 lactghmga 19424 pmtrmvd 19475 mpfrcl 22110 mhpsclcl 22152 fsubbas 23876 filuni 23894 ptcmplem2 24062 itg1climres 25750 mbfi1fseqlem4 25754 dvferm1lem 26023 dvferm2lem 26025 dvferm 26027 dvivthlem1 26048 coeeq2 26282 coe1termlem 26298 isppw 27158 dchrelbasd 27284 lgsne0 27380 wlkvv 29646 eldm3 35762 brfvimex 44044 brovmptimex 44045 clsneibex 44120 neicvgbex 44130 iotan0aiotaex 47110 afvnufveq 47164 gricrcl 47888 grlicrcl 47972 grilcbri2 47976 fvconstr 48770 fvconstrn0 48771 fvconstr2 48772 | 
| Copyright terms: Public domain | W3C validator |