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

Theorem eqcoms 2040
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 2039 . 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 1242
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 1333  ax-gen 1335  ax-ext 2019
This theorem depends on definitions:  df-bi 110  df-cleq 2030
This theorem is referenced by:  gencbvex  2594  gencbval  2596  sbceq2a  2768  eqimss2  2992  uneqdifeqim  3302  tppreq3  3464  copsex2t  3973  copsex2g  3974  ordsoexmid  4240  ordpwsucexmid  4246  cnveqb  4719  cnveq0  4720  relcoi1  4792  funtpg  4893  f1ocnvfv  5362  f1ocnvfvb  5363  cbvfo  5368  cbvexfo  5369  brabvv  5493  ov6g  5580  ectocld  6108  ecoptocl  6129  nn0ind-raph  8111  nn01to3  8308  rennim  9191  bj-inf2vnlem2  9401
  Copyright terms: Public domain W3C validator