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 2957 | . 2 ⊢ (𝐴 ≠ 𝐵 → ¬ ¬ 𝜑) |
3 | 2 | notnotrd 135 | 1 ⊢ (𝐴 ≠ 𝐵 → 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 = wceq 1543 ≠ wne 2932 |
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 210 df-ne 2933 |
This theorem is referenced by: necon1i 2965 opnz 5342 inisegn0 5946 iotan0 6348 tz6.12i 6721 fvfundmfvn0 6733 brfvopabrbr 6793 elfvmptrab1 6823 brovpreldm 7835 brovex 7942 brwitnlem 8212 cantnflem1 9282 carddomi2 9551 rankcf 10356 1re 10798 eliooxr 12958 iccssioo2 12973 elfzoel1 13206 elfzoel2 13207 ismnd 18130 lactghmga 18751 pmtrmvd 18802 mpfrcl 20999 mhpsclcl 21041 fsubbas 22718 filuni 22736 ptcmplem2 22904 itg1climres 24566 mbfi1fseqlem4 24570 dvferm1lem 24835 dvferm2lem 24837 dvferm 24839 dvivthlem1 24859 coeeq2 25090 coe1termlem 25106 isppw 25950 dchrelbasd 26074 lgsne0 26170 wlkvv 27668 eldm3 33398 brfvimex 41254 brovmptimex 41255 clsneibex 41330 neicvgbex 41340 iotan0aiotaex 44200 afvnufveq 44254 fvconstr 45799 fvconstrn0 45800 fvconstr2 45801 |
Copyright terms: Public domain | W3C validator |