ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  neii Unicode version

Theorem neii 2311
Description: Inference associated with df-ne 2310. (Contributed by BJ, 7-Jul-2018.)
Hypothesis
Ref Expression
neii.1  |-  A  =/= 
B
Assertion
Ref Expression
neii  |-  -.  A  =  B

Proof of Theorem neii
StepHypRef Expression
1 neii.1 . 2  |-  A  =/= 
B
2 df-ne 2310 . 2  |-  ( A  =/=  B  <->  -.  A  =  B )
31, 2mpbi 144 1  |-  -.  A  =  B
Colors of variables: wff set class
Syntax hints:   -. wn 3    = wceq 1332    =/= wne 2309
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105
This theorem depends on definitions:  df-bi 116  df-ne 2310
This theorem is referenced by:  2dom  6706  updjudhcoinrg  6973  omp1eomlem  6986  exmidomni  7021  mkvprop  7039  exmidfodomrlemr  7074  exmidfodomrlemrALT  7075  exmidaclem  7080  ine0  8179  inelr  8369  xrltnr  9595  pnfnlt  9602  xrlttri3  9612  nltpnft  9626  xrpnfdc  9654  xrmnfdc  9655  xleaddadd  9699  zfz1iso  10615  3lcm2e6woprm  11801  6lcm4e12  11802  unct  11989  pwle2  13364  subctctexmid  13367  pw1nct  13369  peano3nninf  13374  nninfsellemqall  13384  nninffeq  13389
  Copyright terms: Public domain W3C validator