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

Theorem addcomd 7144
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 (𝜑𝐴 ∈ ℂ)
addcomd.2 (𝜑𝐵 ∈ ℂ)
Assertion
Ref Expression
addcomd (𝜑 → (𝐴 + 𝐵) = (𝐵 + 𝐴))

Proof of Theorem addcomd
StepHypRef Expression
1 muld.1 . 2 (𝜑𝐴 ∈ ℂ)
2 addcomd.2 . 2 (𝜑𝐵 ∈ ℂ)
3 addcom 7130 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) = (𝐵 + 𝐴))
41, 2, 3syl2anc 391 1 (𝜑 → (𝐴 + 𝐵) = (𝐵 + 𝐴))
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1243  wcel 1393  (class class class)co 5499  cc 6868   + caddc 6873
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 101  ax-addcom 6965
This theorem is referenced by:  subadd2  7195  pncan  7197  npcan  7200  subcan  7245  ltadd1  7402  leadd2  7404  ltsubadd2  7406  lesubadd2  7408  mulreim  7571  apadd2  7576  recp1lt1  7841  ltaddrp2d  8624  lincmb01cmp  8838  iccf1o  8839  expaddzap  9177  remullem  9349  resqrexlemover  9486  climaddc2  9727  clim2iser2  9735
  Copyright terms: Public domain W3C validator