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

Theorem necon1ai 2488
Description: Contrapositive inference for inequality. (Contributed by NM, 12-Feb-2007.)
Hypothesis
Ref Expression
necon1ai.1  |-  ( -. 
ph  ->  A  =  B )
Assertion
Ref Expression
necon1ai  |-  ( A  =/=  B  ->  ph )

Proof of Theorem necon1ai
StepHypRef Expression
1 df-ne 2448 . 2  |-  ( A  =/=  B  <->  -.  A  =  B )
2 necon1ai.1 . . 3  |-  ( -. 
ph  ->  A  =  B )
32con1i 121 . 2  |-  ( -.  A  =  B  ->  ph )
41, 3sylbi 187 1  |-  ( A  =/=  B  ->  ph )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1623    =/= wne 2446
This theorem is referenced by:  necon1i  2490  opnz  4242  tz6.12i  5548  elfvdm  5554  brwitnlem  6506  cantnflem1  7391  carddomi2  7603  cdainf  7818  rankcf  8399  1re  8837  eliooxr  10709  iccssioo2  10722  elfzoel1  10873  elfzoel2  10874  ismnd  14369  lactghmga  14784  fsubbas  17562  filuni  17580  ptcmplem2  17747  itg1climres  19069  mbfi1fseqlem4  19073  dvferm1lem  19331  dvferm2lem  19333  dvferm  19335  dvivthlem1  19355  mpfrcl  19402  coeeq2  19624  coe1termlem  19639  isppw  20352  dchrelbasd  20478  lgsne0  20572  eldm3  24119  inisegn0  27140  pmtrmvd  27398  fvfundmfvn0  27986  afvnufveq  28010
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-ne 2448
  Copyright terms: Public domain W3C validator