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

Theorem com15 93
Description: Commutation of antecedents. Swap 1st and 5th. (Contributed by Jeff Hankins, 28-Jun-2009.) (Proof shortened by Wolf Lammen, 29-Jul-2012.)
Hypothesis
Ref Expression
com5.1
Assertion
Ref Expression
com15

Proof of Theorem com15
StepHypRef Expression
1 com5.1 . . 3
21com5l 92 . 2
32com4r 86 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4
This theorem is referenced by:  injresinjlem  11925  brfi1uzind  12532  swrdswrdlem  12684  2cshwcshw  12793  spthonepeq  24589  wlkdvspthlem  24609  erclwwlktr  24815  erclwwlkntr  24827  el2wlkonot  24869  3cyclfrgrarn1  25012  frgranbnb  25020  vdn0frgrav2  25023  frgrancvvdeqlemB  25038  usg2spot2nb  25065  numclwwlkovf2ex  25086  frgrareg  25117  frgraregord013  25118  zerdivemp1  25436  zerdivemp1x  30358  usgra2pthlem1  32353  initoeu1  32617  initoeu2lem1  32620  initoeu2  32622  termoeu1  32624
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
  Copyright terms: Public domain W3C validator