![]() |
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 2989 | . 2 ⊢ (𝐴 ≠ 𝐵 → ¬ ¬ 𝜑) |
3 | 2 | notnotrd 131 | 1 ⊢ (𝐴 ≠ 𝐵 → 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 = wceq 1507 ≠ wne 2964 |
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 199 df-ne 2965 |
This theorem is referenced by: necon1i 2997 opnz 5219 inisegn0 5799 tz6.12i 6523 elfvdmOLD 6530 fvfundmfvn0 6536 brfvopabrbr 6590 elfvmptrab1 6618 brovpreldm 7589 brovex 7688 brwitnlem 7930 cantnflem1 8942 carddomi2 9189 rankcf 9993 1re 10435 eliooxr 12608 iccssioo2 12622 elfzoel1 12849 elfzoel2 12850 ismnd 17759 lactghmga 18287 pmtrmvd 18339 mpfrcl 20005 fsubbas 22173 filuni 22191 ptcmplem2 22359 itg1climres 24012 mbfi1fseqlem4 24016 dvferm1lem 24278 dvferm2lem 24280 dvferm 24282 dvivthlem1 24302 coeeq2 24529 coe1termlem 24545 isppw 25387 dchrelbasd 25511 lgsne0 25607 wlkvv 27105 eldm3 32487 brfvimex 39717 brovmptimex 39718 clsneibex 39793 neicvgbex 39803 iotan0aiotaex 42676 afvnufveq 42731 |
Copyright terms: Public domain | W3C validator |