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 3020 | . . 3 ⊢ (¬ 𝐴 ≠ 𝐵 ↔ 𝐴 = 𝐵) | |
2 | necon3bd.1 | . . 3 ⊢ (𝜑 → (𝐴 = 𝐵 → 𝜓)) | |
3 | 1, 2 | syl5bi 243 | . 2 ⊢ (𝜑 → (¬ 𝐴 ≠ 𝐵 → 𝜓)) |
4 | 3 | con1d 147 | 1 ⊢ (𝜑 → (¬ 𝜓 → 𝐴 ≠ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 = wceq 1528 ≠ wne 3016 |
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 208 df-ne 3017 |
This theorem is referenced by: necon2ad 3031 nelne1OLD 3114 nelne2OLD 3116 nssne1 4026 nssne2 4027 disjne 4402 nbrne1 5077 nbrne2 5078 peano5 7593 oeeui 8218 domdifsn 8589 ac6sfi 8751 inf3lem2 9081 cnfcom3lem 9155 dfac9 9551 fin23lem21 9750 dedekindle 10793 zneo 12054 modirr 13300 sqrmo 14601 reusq0 14812 pc2dvds 16205 pcadd 16215 oddprmdvds 16229 4sqlem11 16281 latnlej 17668 sylow2blem3 18678 irredn0 19384 irredn1 19387 lssvneln0 19654 lspsnne2 19821 lspfixed 19831 lspindpi 19835 lsmcv 19844 lspsolv 19846 isnzr2 19966 coe1tmmul 20375 dfac14 22156 fbdmn0 22372 filufint 22458 flimfnfcls 22566 alexsubALTlem2 22586 evth 23492 cphsqrtcl2 23719 ovolicc2lem4 24050 lhop1lem 24539 lhop1 24540 lhop2 24541 lhop 24542 deg1add 24626 abelthlem2 24949 logcnlem2 25153 angpined 25335 asinneg 25391 dmgmaddn0 25528 lgsne0 25839 lgsqr 25855 lgsquadlem2 25885 lgsquadlem3 25886 axlowdimlem17 26672 spansncvi 29357 broutsideof2 33481 unblimceq0lem 33743 poimirlem28 34802 dvasin 34860 dvacos 34861 nninfnub 34909 dvrunz 35115 lsatcvatlem 36067 lkrlsp2 36121 opnlen0 36206 2llnne2N 36426 lnnat 36445 llnn0 36534 lplnn0N 36565 lplnllnneN 36574 llncvrlpln2 36575 llncvrlpln 36576 lvoln0N 36609 lplncvrlvol2 36633 lplncvrlvol 36634 dalempnes 36669 dalemqnet 36670 dalemcea 36678 dalem3 36682 cdlema1N 36809 cdlemb 36812 paddasslem5 36842 llnexchb2lem 36886 osumcllem4N 36977 pexmidlem1N 36988 lhp2lt 37019 lhp2atne 37052 lhp2at0ne 37054 4atexlemunv 37084 4atexlemex2 37089 trlne 37203 trlval4 37206 cdlemc4 37212 cdleme11dN 37280 cdleme11h 37284 cdlemednuN 37318 cdleme20j 37336 cdleme20k 37337 cdleme21at 37346 cdleme35f 37472 cdlemg11b 37660 dia2dimlem1 38082 dihmeetlem3N 38323 dihmeetlem15N 38339 dochsnnz 38468 dochexmidlem1 38478 dochexmidlem7 38484 mapdindp3 38740 fltne 39152 pellexlem1 39306 dfac21 39546 pm13.14 40621 uzlidlring 44098 suppdm 44463 |
Copyright terms: Public domain | W3C validator |