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

Theorem necon1ai 2623
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 2620 . 2  |-  ( A  =/=  B  ->  -.  -.  ph )
32notnotrd 113 1  |-  ( A  =/=  B  ->  ph )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1399    =/= wne 2587
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 2589
This theorem is referenced by:  necon1i  2634  opnz  4646  tz6.12i  5807  elfvdm  5813  fvfundmfvn0  5819  elfvmptrab1  5891  bropopvvv  6797  brovex  6886  brwitnlem  7093  cantnflem1  8039  cantnflem1OLD  8062  carddomi2  8282  cdainf  8503  rankcf  9084  1re  9524  eliooxr  11522  iccssioo2  11536  elfzoel1  11738  elfzoel2  11739  ismnd  16059  ismndOLD  16062  lactghmga  16565  pmtrmvd  16617  mpfrcl  18319  fsubbas  20472  filuni  20490  ptcmplem2  20657  itg1climres  22225  mbfi1fseqlem4  22229  dvferm1lem  22489  dvferm2lem  22491  dvferm  22493  dvivthlem1  22513  coeeq2  22743  coe1termlem  22759  isppw  23524  dchrelbasd  23650  lgsne0  23744  clwwlknprop  24914  2wlkonot3v  25017  2spthonot3v  25018  eldm3  29393  inisegn0  31191  afvnufveq  32433
  Copyright terms: Public domain W3C validator