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

Theorem necon1ai 2698
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 2695 . 2  |-  ( A  =/=  B  ->  -.  -.  ph )
32notnotrd 113 1  |-  ( A  =/=  B  ->  ph )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1379    =/= wne 2662
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 2664
This theorem is referenced by:  necon1i  2709  opnz  4718  tz6.12i  5884  elfvdm  5890  fvfundmfvn0  5896  elfvmptrab1  5968  bropopvvv  6860  brovex  6947  brwitnlem  7154  cantnflem1  8104  cantnflem1OLD  8127  carddomi2  8347  cdainf  8568  rankcf  9151  1re  9591  eliooxr  11579  iccssioo2  11593  elfzoel1  11791  elfzoel2  11792  ismnd  15730  lactghmga  16224  pmtrmvd  16277  mpfrcl  17958  fsubbas  20103  filuni  20121  ptcmplem2  20288  itg1climres  21856  mbfi1fseqlem4  21860  dvferm1lem  22120  dvferm2lem  22122  dvferm  22124  dvivthlem1  22144  coeeq2  22374  coe1termlem  22389  isppw  23116  dchrelbasd  23242  lgsne0  23336  clwwlknprop  24448  2wlkonot3v  24551  2spthonot3v  24552  eldm3  28768  inisegn0  30593  afvnufveq  31699
  Copyright terms: Public domain W3C validator