MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  necon1ad Structured version   Unicode version

Theorem necon1ad 2673
Description: Contrapositive deduction for inequality. (Contributed by NM, 2-Apr-2007.) (Proof shortened by Wolf Lammen, 23-Nov-2019.)
Hypothesis
Ref Expression
necon1ad.1  |-  ( ph  ->  ( -.  ps  ->  A  =  B ) )
Assertion
Ref Expression
necon1ad  |-  ( ph  ->  ( A  =/=  B  ->  ps ) )

Proof of Theorem necon1ad
StepHypRef Expression
1 necon1ad.1 . . 3  |-  ( ph  ->  ( -.  ps  ->  A  =  B ) )
21necon3ad 2667 . 2  |-  ( ph  ->  ( A  =/=  B  ->  -.  -.  ps )
)
3 notnot2 112 . 2  |-  ( -. 
-.  ps  ->  ps )
42, 3syl6 33 1  |-  ( ph  ->  ( A  =/=  B  ->  ps ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1395    =/= wne 2652
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 185  df-ne 2654
This theorem is referenced by:  prnebg  4214  fr0  4867  sofld  5461  suppssOLD  6021  suppss2OLD  6529  onmindif2  6646  suppss  6948  suppss2  6952  uniinqs  7409  dfac5lem4  8524  uzwo  11169  seqf1olem1  12148  seqf1olem2  12149  hashnncl  12438  pceq0  14405  vdwmc2  14508  odcau  16750  islss  17707  fidomndrnglem  18081  mvrf1  18207  mpfrcl  18313  obs2ss  18886  obslbs  18887  dsmmacl  18898  regr1lem2  20366  iccpnfhmeo  21570  itg10a  22242  dvlip  22519  deg1ge  22624  elply2  22718  coeeulem  22746  dgrle  22765  coemullem  22772  basellem2  23480  perfectlem2  23630  lgsabs1  23734  lnon0  25839  atsseq  27392  disjif2  27579  suppss2f  27620  cvmseu  28896  itg2addnclem  30228  lsatcmp  34829  lsatcmp2  34830  ltrnnid  35961  trlatn0  35998  cdlemh  36644  dochlkr  37213
  Copyright terms: Public domain W3C validator