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

Theorem neii 2349
Description: Inference associated with df-ne 2348. (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 2348 . 2  |-  ( A  =/=  B  <->  -.  A  =  B )
31, 2mpbi 145 1  |-  -.  A  =  B
Colors of variables: wff set class
Syntax hints:   -. wn 3    = wceq 1353    =/= wne 2347
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106
This theorem depends on definitions:  df-bi 117  df-ne 2348
This theorem is referenced by:  2dom  6798  updjudhcoinrg  7073  omp1eomlem  7086  nninfisol  7124  exmidomni  7133  mkvprop  7149  nninfwlporlemd  7163  nninfwlpoimlemginf  7167  exmidfodomrlemr  7194  exmidfodomrlemrALT  7195  exmidaclem  7200  ine0  8328  inelr  8518  xrltnr  9753  pnfnlt  9761  xrlttri3  9771  nltpnft  9788  xrpnfdc  9816  xrmnfdc  9817  xleaddadd  9861  zfz1iso  10792  3lcm2e6woprm  12056  6lcm4e12  12057  m1dvdsndvds  12218  unct  12413  bj-charfunbi  14185  pwle2  14370  subctctexmid  14373  pw1nct  14375  peano3nninf  14379  nninfsellemqall  14387  nninffeq  14392
  Copyright terms: Public domain W3C validator