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

Theorem necon1ai 2674
Description: Contrapositive inference for inequality. (Contributed by NM, 12-Feb-2007.) (Proof shortened by Wolf Lammen, 22-Nov-2019.)
Hypothesis
Ref Expression
necon1ai.1  |-  ( -. 
ph  ->  A  =  B )
Assertion
Ref Expression
necon1ai  |-  ( A  =/=  B  ->  ph )

Proof of Theorem necon1ai
StepHypRef Expression
1 necon1ai.1 . . 3  |-  ( -. 
ph  ->  A  =  B )
21necon3ai 2671 . 2  |-  ( A  =/=  B  ->  -.  -.  ph )
32notnotrd 113 1  |-  ( A  =/=  B  ->  ph )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1383    =/= wne 2638
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 2640
This theorem is referenced by:  necon1i  2685  opnz  4708  tz6.12i  5876  elfvdm  5882  fvfundmfvn0  5888  elfvmptrab1  5961  bropopvvv  6865  brovex  6952  brwitnlem  7159  cantnflem1  8111  cantnflem1OLD  8134  carddomi2  8354  cdainf  8575  rankcf  9158  1re  9598  eliooxr  11594  iccssioo2  11608  elfzoel1  11809  elfzoel2  11810  ismnd  15902  ismndOLD  15905  lactghmga  16408  pmtrmvd  16460  mpfrcl  18166  fsubbas  20346  filuni  20364  ptcmplem2  20531  itg1climres  22099  mbfi1fseqlem4  22103  dvferm1lem  22363  dvferm2lem  22365  dvferm  22367  dvivthlem1  22387  coeeq2  22617  coe1termlem  22633  isppw  23366  dchrelbasd  23492  lgsne0  23586  clwwlknprop  24750  2wlkonot3v  24853  2spthonot3v  24854  eldm3  29167  inisegn0  30965  afvnufveq  32186
  Copyright terms: Public domain W3C validator