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

Theorem addcomd 6941
Description: Addition commutes. Based on ideas by Eric Schmidt. (Contributed by Scott Fenton, 3-Jan-2013.) (Revised by Mario Carneiro, 27-May-2016.)
Hypotheses
Ref Expression
muld.1 (φA ℂ)
addcomd.2 (φB ℂ)
Assertion
Ref Expression
addcomd (φ → (A + B) = (B + A))

Proof of Theorem addcomd
StepHypRef Expression
1 muld.1 . 2 (φA ℂ)
2 addcomd.2 . 2 (φB ℂ)
3 addcom 6927 . 2 ((A B ℂ) → (A + B) = (B + A))
41, 2, 3syl2anc 391 1 (φ → (A + B) = (B + A))
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1242   wcel 1390  (class class class)co 5455  cc 6689   + caddc 6694
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 101  ax-addcom 6763
This theorem is referenced by:  subadd2  6992  pncan  6994  npcan  6997  subcan  7042  ltadd1  7199  leadd2  7201  ltsubadd2  7203  lesubadd2  7205  mulreim  7368  apadd2  7373  recp1lt1  7626  ltaddrp2d  8407  lincmb01cmp  8621  iccf1o  8622  expaddzap  8933  remullem  9079
  Copyright terms: Public domain W3C validator