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

Theorem necon1ai 2676
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 2673 . 2  |-  ( A  =/=  B  ->  -.  -.  ph )
32notnotrd 113 1  |-  ( A  =/=  B  ->  ph )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1370    =/= wne 2641
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 2643
This theorem is referenced by:  necon1i  2687  opnz  4647  tz6.12i  5795  elfvdm  5801  fvfundmfvn0  5807  bropopvvv  6739  brovex  6826  brwitnlem  7033  cantnflem1  7984  cantnflem1OLD  8007  carddomi2  8227  cdainf  8448  rankcf  9031  1re  9472  eliooxr  11441  iccssioo2  11455  elfzoel1  11638  elfzoel2  11639  ismnd  15505  lactghmga  15997  pmtrmvd  16050  mpfrcl  17697  fsubbas  19542  filuni  19560  ptcmplem2  19727  itg1climres  21294  mbfi1fseqlem4  21298  dvferm1lem  21558  dvferm2lem  21560  dvferm  21562  dvivthlem1  21582  coeeq2  21812  coe1termlem  21827  isppw  22554  dchrelbasd  22680  lgsne0  22774  eldm3  27692  inisegn0  29520  afvnufveq  30177  elfvmptrab1  30278  2wlkonot3v  30518  2spthonot3v  30519  clwwlknprop  30559
  Copyright terms: Public domain W3C validator