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

Theorem necomd 2395
 Description: Deduction from commutative law for inequality. (Contributed by NM, 12-Feb-2008.)
Hypothesis
Ref Expression
necomd.1 (𝜑𝐴𝐵)
Assertion
Ref Expression
necomd (𝜑𝐵𝐴)

Proof of Theorem necomd
StepHypRef Expression
1 necomd.1 . 2 (𝜑𝐴𝐵)
2 necom 2393 . 2 (𝐴𝐵𝐵𝐴)
31, 2sylib 121 1 (𝜑𝐵𝐴)
 Colors of variables: wff set class Syntax hints:   → wi 4   ≠ wne 2309 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-5 1424  ax-gen 1426  ax-ext 2122 This theorem depends on definitions:  df-bi 116  df-cleq 2133  df-ne 2310 This theorem is referenced by:  difsnb  3672  0nelop  4179  frecabcl  6305  fidifsnen  6773  tpfidisj  6826  omp1eomlem  6989  difinfsnlem  6994  fodjuomnilemdc  7026  en2eleq  7071  en2other2  7072  ltned  7921  lt0ne0  8234  zdceq  9170  zneo  9196  xrlttri3  9633  qdceq  10075  flqltnz  10111  nn0opthd  10520  hashdifpr  10618  sumtp  11235  isprm2lem  11853  ennnfonelemex  11983
 Copyright terms: Public domain W3C validator