HOLE Home Higher-Order Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  HOLE Home  >  Th. List  >  eqcomi GIF version

Theorem eqcomi 79
Description: Commutativity of equality. (Contributed by Mario Carneiro, 7-Oct-2014.)
Hypotheses
Ref Expression
eqcomi.1 A:α
eqcomi.2 R⊧[A = B]
Assertion
Ref Expression
eqcomi R⊧[B = A]

Proof of Theorem eqcomi
StepHypRef Expression
1 weq 41 . 2 = :(α → (α → ∗))
2 eqcomi.1 . . 3 A:α
3 eqcomi.2 . . 3 R⊧[A = B]
42, 3eqtypi 78 . 2 B:α
51, 2, 4, 3dfov1 74 . . 3 R⊧(( = A)B)
62, 4, 5eqcomx 52 . 2 R⊧(( = B)A)
71, 4, 2, 6dfov2 75 1 R⊧[B = A]
Colors of variables: type var term
Syntax hints:   = ke 7  [kbr 9  wffMMJ2 11  wffMMJ2t 12
This theorem was proved from axioms:  ax-syl 15  ax-jca 17  ax-trud 26  ax-cb1 29  ax-cb2 30  ax-weq 40  ax-refl 42  ax-eqmp 45  ax-wc 49  ax-ceq 51  ax-wov 71  ax-eqtypi 77
This theorem depends on definitions:  df-ov 73
This theorem is referenced by:  mpbir  87  3eqtr4i  96  3eqtr3i  97  hbth  109  alrimiv  151  dfan2  154  hbct  155  olc  164  orc  165  exlimdv  167  cbvf  179  alrimi  182  exlimd  183  exmid  199  exnal  201  ax8  211  ax9  212  ax10  213
  Copyright terms: Public domain W3C validator