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

Theorem necon1ai 2501
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 2461 . 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 1632    =/= wne 2459
This theorem is referenced by:  necon1i  2503  opnz  4258  tz6.12i  5564  elfvdm  5570  brwitnlem  6522  cantnflem1  7407  carddomi2  7619  cdainf  7834  rankcf  8415  1re  8853  eliooxr  10725  iccssioo2  10738  elfzoel1  10889  elfzoel2  10890  ismnd  14385  lactghmga  14800  fsubbas  17578  filuni  17596  ptcmplem2  17763  itg1climres  19085  mbfi1fseqlem4  19089  dvferm1lem  19347  dvferm2lem  19349  dvferm  19351  dvivthlem1  19371  mpfrcl  19418  coeeq2  19640  coe1termlem  19655  isppw  20368  dchrelbasd  20494  lgsne0  20588  eldm3  24190  inisegn0  27243  pmtrmvd  27501  fvfundmfvn0  28091  afvnufveq  28115  brovex  28205  trlonprop  28341
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 2461
  Copyright terms: Public domain W3C validator