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

Theorem addcomd 6921
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 6907 . 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 6669   + caddc 6674
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 101  ax-addcom 6743
This theorem is referenced by:  subadd2  6972  pncan  6974  npcan  6977  subcan  7022  ltadd1  7179  leadd2  7181  ltsubadd2  7183  lesubadd2  7185  mulreim  7348  apadd2  7353  recp1lt1  7606  ltaddrp2d  8387  lincmb01cmp  8601  iccf1o  8602  expaddzap  8913  remullem  9059
  Copyright terms: Public domain W3C validator