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

Theorem necon1ai 2640
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 2600 . 2  |-  ( A  =/=  B  <->  -.  A  =  B )
2 necon1ai.1 . . 3  |-  ( -. 
ph  ->  A  =  B )
32con1i 123 . 2  |-  ( -.  A  =  B  ->  ph )
41, 3sylbi 188 1  |-  ( A  =/=  B  ->  ph )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1652    =/= wne 2598
This theorem is referenced by:  necon1i  2642  opnz  4424  tz6.12i  5743  elfvdm  5749  fvfundmfvn0  5754  bropopvvv  6418  brovex  6466  brwitnlem  6743  cantnflem1  7637  carddomi2  7849  cdainf  8064  rankcf  8644  1re  9082  eliooxr  10961  iccssioo2  10975  elfzoel1  11130  elfzoel2  11131  ismnd  14684  lactghmga  15099  fsubbas  17891  filuni  17909  ptcmplem2  18076  itg1climres  19598  mbfi1fseqlem4  19602  dvferm1lem  19860  dvferm2lem  19862  dvferm  19864  dvivthlem1  19884  mpfrcl  19931  coeeq2  20153  coe1termlem  20168  isppw  20889  dchrelbasd  21015  lgsne0  21109  eldm3  25377  inisegn0  27109  pmtrmvd  27366  afvnufveq  27978  2wlkonot3v  28295  2spthonot3v  28296
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 178  df-ne 2600
  Copyright terms: Public domain W3C validator