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

Theorem eqcoms 2059
 Description: Inference applying commutative law for class equality to an antecedent. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
eqcoms.1 (𝐴 = 𝐵𝜑)
Assertion
Ref Expression
eqcoms (𝐵 = 𝐴𝜑)

Proof of Theorem eqcoms
StepHypRef Expression
1 eqcom 2058 . 2 (𝐵 = 𝐴𝐴 = 𝐵)
2 eqcoms.1 . 2 (𝐴 = 𝐵𝜑)
31, 2sylbi 118 1 (𝐵 = 𝐴𝜑)
 Colors of variables: wff set class Syntax hints:   → wi 4   = wceq 1259 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1352  ax-gen 1354  ax-ext 2038 This theorem depends on definitions:  df-bi 114  df-cleq 2049 This theorem is referenced by:  gencbvex  2617  gencbval  2619  sbceq2a  2797  eqimss2  3026  uneqdifeqim  3336  tppreq3  3501  copsex2t  4010  copsex2g  4011  ordsoexmid  4314  0elsucexmid  4317  ordpwsucexmid  4322  cnveqb  4804  cnveq0  4805  relcoi1  4877  funtpg  4978  f1ocnvfv  5447  f1ocnvfvb  5448  cbvfo  5453  cbvexfo  5454  brabvv  5579  ov6g  5666  ectocld  6203  ecoptocl  6224  phplem3  6348  nn0ind-raph  8414  nn01to3  8649  modqmuladd  9316  modqmuladdnn0  9318  rennim  9829  m1expe  10211  m1expo  10212  m1exp1  10213  nn0o1gt2  10217  flodddiv4  10246  bj-inf2vnlem2  10483
 Copyright terms: Public domain W3C validator