![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > necon3ad | 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.) (Proof shortened by Wolf Lammen, 23-Nov-2019.) |
Ref | Expression |
---|---|
necon3ad.1 | ⊢ (𝜑 → (𝜓 → 𝐴 = 𝐵)) |
Ref | Expression |
---|---|
necon3ad | ⊢ (𝜑 → (𝐴 ≠ 𝐵 → ¬ 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | necon3ad.1 | . 2 ⊢ (𝜑 → (𝜓 → 𝐴 = 𝐵)) | |
2 | neneq 2975 | . 2 ⊢ (𝐴 ≠ 𝐵 → ¬ 𝐴 = 𝐵) | |
3 | 1, 2 | nsyli 157 | 1 ⊢ (𝜑 → (𝐴 ≠ 𝐵 → ¬ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 = wceq 1601 ≠ wne 2969 |
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 2970 |
This theorem is referenced by: necon1ad 2986 necon3d 2990 disjpss 4253 2f1fvneq 6789 oeeulem 7965 enp1i 8483 canthp1lem2 9810 winalim2 9853 nlt1pi 10063 sqreulem 14506 rpnnen2lem11 15357 eucalglt 15704 nprm 15806 pcprmpw2 15990 pcmpt 16000 expnprm 16010 prmlem0 16211 pltnle 17352 psgnunilem1 18296 pgpfi 18404 frgpnabllem1 18662 gsumval3a 18690 ablfac1eulem 18858 pgpfaclem2 18868 lspdisjb 19521 lspdisj2 19522 obselocv 20471 0nnei 21324 t0dist 21537 t1sep 21582 ordthauslem 21595 hausflim 22193 bcthlem5 23534 bcth 23535 fta1g 24364 plyco0 24385 dgrnznn 24440 coeaddlem 24442 fta1 24500 vieta1lem2 24503 logcnlem3 24827 dvloglem 24831 dcubic 25024 mumullem2 25358 2sqlem8a 25602 dchrisum0flblem1 25649 colperpexlem2 26079 elntg2 26334 1loopgrnb0 26850 usgr2trlncrct 27155 ocnel 28729 hatomistici 29793 lbslsat 30432 sibfof 31000 outsideofrflx 32823 poimirlem23 34058 mblfinlem1 34072 cntotbnd 34219 heiborlem6 34239 lshpnel 35137 lshpcmp 35142 lfl1 35224 lkrshp 35259 lkrpssN 35317 atnlt 35467 atnle 35471 atlatmstc 35473 intnatN 35561 atbtwn 35600 llnnlt 35677 lplnnlt 35719 2llnjaN 35720 lvolnltN 35772 2lplnja 35773 dalem-cly 35825 dalem44 35870 2llnma3r 35942 cdlemblem 35947 lhpm0atN 36183 lhp2atnle 36187 cdlemednpq 36453 cdleme22cN 36496 cdlemg18b 36833 cdlemg42 36883 dia2dimlem1 37218 dochkrshp 37540 hgmapval0 38046 rrx2pnecoorneor 43451 |
Copyright terms: Public domain | W3C validator |