![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > necon3bd | Structured version Visualization version GIF version |
Description: Contrapositive law deduction for inequality. (Contributed by NM, 2-Apr-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.) |
Ref | Expression |
---|---|
necon3bd.1 | ⊢ (𝜑 → (𝐴 = 𝐵 → 𝜓)) |
Ref | Expression |
---|---|
necon3bd | ⊢ (𝜑 → (¬ 𝜓 → 𝐴 ≠ 𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nne 2933 | . . 3 ⊢ (¬ 𝐴 ≠ 𝐵 ↔ 𝐴 = 𝐵) | |
2 | necon3bd.1 | . . 3 ⊢ (𝜑 → (𝐴 = 𝐵 → 𝜓)) | |
3 | 1, 2 | biimtrid 241 | . 2 ⊢ (𝜑 → (¬ 𝐴 ≠ 𝐵 → 𝜓)) |
4 | 3 | con1d 145 | 1 ⊢ (𝜑 → (¬ 𝜓 → 𝐴 ≠ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 = wceq 1533 ≠ wne 2929 |
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 2930 |
This theorem is referenced by: necon2ad 2944 nssne1 4039 nssne2 4040 disjne 4456 nbrne1 5168 nbrne2 5169 peano5 7900 peano5OLD 7901 oeeui 8623 domdifsn 9079 ac6sfi 9312 inf3lem2 9654 cnfcom3lem 9728 dfac9 10161 fin23lem21 10364 dedekindle 11410 zneo 12678 modirr 13943 sqrmo 15234 reusq0 15445 pc2dvds 16851 pcadd 16861 oddprmdvds 16875 4sqlem11 16927 latnlej 18451 sylow2blem3 19589 irredn0 20374 irredn1 20377 isnzr2 20469 lssvneln0 20848 lspsnne2 21018 lspfixed 21028 lspindpi 21032 lsmcv 21041 lspsolv 21043 coe1tmmul 22221 dfac14 23566 fbdmn0 23782 filufint 23868 flimfnfcls 23976 alexsubALTlem2 23996 evth 24929 cphsqrtcl2 25158 ovolicc2lem4 25493 lhop1lem 25990 lhop1 25991 lhop2 25992 lhop 25993 deg1add 26083 abelthlem2 26414 logcnlem2 26622 angpined 26807 asinneg 26863 dmgmaddn0 27000 lgsne0 27313 lgsqr 27329 lgsquadlem2 27359 lgsquadlem3 27360 axlowdimlem17 28841 spansncvi 31534 zarcmplem 33610 broutsideof2 35846 unblimceq0lem 36109 poimirlem28 37249 dvasin 37305 dvacos 37306 nninfnub 37352 dvrunz 37555 lsatcvatlem 38648 lkrlsp2 38702 opnlen0 38787 2llnne2N 39008 lnnat 39027 llnn0 39116 lplnn0N 39147 lplnllnneN 39156 llncvrlpln2 39157 llncvrlpln 39158 lvoln0N 39191 lplncvrlvol2 39215 lplncvrlvol 39216 dalempnes 39251 dalemqnet 39252 dalemcea 39260 dalem3 39264 cdlema1N 39391 cdlemb 39394 paddasslem5 39424 llnexchb2lem 39468 osumcllem4N 39559 pexmidlem1N 39570 lhp2lt 39601 lhp2atne 39634 lhp2at0ne 39636 4atexlemunv 39666 4atexlemex2 39671 trlne 39785 trlval4 39788 cdlemc4 39794 cdleme11dN 39862 cdleme11h 39866 cdlemednuN 39900 cdleme20j 39918 cdleme20k 39919 cdleme21at 39928 cdleme35f 40054 cdlemg11b 40242 dia2dimlem1 40664 dihmeetlem3N 40905 dihmeetlem15N 40921 dochsnnz 41050 dochexmidlem1 41060 dochexmidlem7 41066 mapdindp3 41322 fltne 42200 pellexlem1 42388 dfac21 42629 pm13.14 43985 uzlidlring 47480 suppdm 47761 |
Copyright terms: Public domain | W3C validator |