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

Theorem eqcoms 2025
Description: Inference applying commutative law for class equality to an antecedent. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
eqcoms.1 (A = Bφ)
Assertion
Ref Expression
eqcoms (B = Aφ)

Proof of Theorem eqcoms
StepHypRef Expression
1 eqcom 2024 . 2 (B = AA = B)
2 eqcoms.1 . 2 (A = Bφ)
31, 2sylbi 114 1 (B = Aφ)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1228
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1316  ax-gen 1318  ax-ext 2004
This theorem depends on definitions:  df-bi 110  df-cleq 2015
This theorem is referenced by:  gencbvex  2577  gencbval  2579  sbceq2a  2751  eqimss2  2975  uneqdifeqim  3285  tppreq3  3447  copsex2t  3956  copsex2g  3957  ordsoexmid  4224  ordpwsucexmid  4230  cnveqb  4703  cnveq0  4704  relcoi1  4776  funtpg  4876  f1ocnvfv  5344  f1ocnvfvb  5345  cbvfo  5350  cbvexfo  5351  brabvv  5474  ov6g  5561  ectocld  6083  ecoptocl  6104  bj-inf2vnlem2  7336
  Copyright terms: Public domain W3C validator