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

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

Proof of Theorem eqcoms
StepHypRef Expression
1 eqcom 2085 . 2  |-  ( B  =  A  <->  A  =  B )
2 eqcoms.1 . 2  |-  ( A  =  B  ->  ph )
31, 2sylbi 119 1  |-  ( B  =  A  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1285
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1377  ax-gen 1379  ax-ext 2065
This theorem depends on definitions:  df-bi 115  df-cleq 2076
This theorem is referenced by:  gencbvex  2654  gencbval  2656  sbceq2a  2834  eqimss2  3061  uneqdifeqim  3344  tppreq3  3513  copsex2t  4028  copsex2g  4029  ordsoexmid  4333  0elsucexmid  4336  ordpwsucexmid  4341  cnveqb  4826  cnveq0  4827  relcoi1  4899  funtpg  5001  f1ocnvfv  5470  f1ocnvfvb  5471  cbvfo  5476  cbvexfo  5477  brabvv  5602  ov6g  5689  ectocld  6259  ecoptocl  6280  phplem3  6410  f1dmvrnfibi  6484  f1vrnfibi  6485  pr2ne  6572  nn0ind-raph  8597  nn01to3  8835  modqmuladd  9500  modqmuladdnn0  9502  fihashf1rn  9865  hashfzp1  9900  rennim  10089  m1expe  10506  m1expo  10507  m1exp1  10508  nn0o1gt2  10512  flodddiv4  10541  cncongr1  10692  bj-inf2vnlem2  11033
  Copyright terms: Public domain W3C validator