MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  tprot Unicode version

Theorem tprot 4125
Description: Rotation of the elements of an unordered triple. (Contributed by Alan Sare, 24-Oct-2011.)
Assertion
Ref Expression
tprot

Proof of Theorem tprot
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 3orrot 979 . . 3
21abbii 2591 . 2
3 dftp2 4075 . 2
4 dftp2 4075 . 2
52, 3, 43eqtr4i 2496 1
Colors of variables: wff setvar class
Syntax hints:  \/w3o 972  =wceq 1395  {cab 2442  {ctp 4033
This theorem is referenced by:  tpcomb  4127  tpass  4128  tpidm13  4132  tpidm23  4133  tpnzd  4152  tpprceq3  4170  fvtp2  6119  fvtp3  6120  fvtp2g  6122  fvtp3g  6123  f13dfv  6180  en3lplem2  8053  nb3graprlem2  24452  nb3grapr  24453  nb3grapr2  24454  nb3gra2nb  24455  cusgra3v  24464  frgra3v  25002  1to3vfriswmgra  25007  estrres  32645  en3lplem2VD  33644  dvh4dimN  37174
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-un 3480  df-sn 4030  df-pr 4032  df-tp 4034
  Copyright terms: Public domain W3C validator