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

Theorem nesymi 2405
Description: Inference associated with nesym 2404. (Contributed by BJ, 7-Jul-2018.)
Hypothesis
Ref Expression
nesymi.1  |-  A  =/= 
B
Assertion
Ref Expression
nesymi  |-  -.  B  =  A

Proof of Theorem nesymi
StepHypRef Expression
1 nesymi.1 . 2  |-  A  =/= 
B
2 nesym 2404 . 2  |-  ( A  =/=  B  <->  -.  B  =  A )
31, 2mpbi 145 1  |-  -.  B  =  A
Colors of variables: wff set class
Syntax hints:   -. wn 3    = wceq 1363    =/= wne 2359
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-5 1457  ax-gen 1459  ax-ext 2170
This theorem depends on definitions:  df-bi 117  df-cleq 2181  df-ne 2360
This theorem is referenced by:  frec0g  6415  djune  7094  omp1eomlem  7110  fodjum  7161  fodju0  7162  ismkvnex  7170  mkvprop  7173  omniwomnimkv  7182  3nelsucpw1  7250  xrltnr  9796  nltmnf  9805  xnn0xadd0  9884  fnpr2ob  12781  pwle2  15132  nninfalllem1  15141  nninfall  15142  nninfsellemeq  15147  trirec0xor  15177
  Copyright terms: Public domain W3C validator