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

Theorem necon1ai 2592
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 2552 . 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 1649    =/= wne 2550
This theorem is referenced by:  necon1i  2594  opnz  4373  tz6.12i  5691  elfvdm  5697  bropopvvv  6365  brovex  6410  brwitnlem  6687  cantnflem1  7578  carddomi2  7790  cdainf  8005  rankcf  8585  1re  9023  eliooxr  10901  iccssioo2  10915  elfzoel1  11068  elfzoel2  11069  ismnd  14619  lactghmga  15034  fsubbas  17820  filuni  17838  ptcmplem2  18005  itg1climres  19473  mbfi1fseqlem4  19477  dvferm1lem  19735  dvferm2lem  19737  dvferm  19739  dvivthlem1  19759  mpfrcl  19806  coeeq2  20028  coe1termlem  20043  isppw  20764  dchrelbasd  20890  lgsne0  20984  eldm3  25143  inisegn0  26809  pmtrmvd  27067  fvfundmfvn0  27656  afvnufveq  27680
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 2552
  Copyright terms: Public domain W3C validator