![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > com25 | Structured version Unicode version |
Description: Commutation of antecedents. Swap 2nd and 5th. (Contributed by Jeff Hankins, 28-Jun-2009.) |
Ref | Expression |
---|---|
com5.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
com25 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | com5.1 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | com24 87 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | com45 89 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 3 | com24 87 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 |
This theorem is referenced by: injresinjlem 11758 brfi1uzind 12340 swrdswrdlem 12474 neindisj2 18862 2ndcdisj 19195 usgrafisinds 23498 cusgrasize2inds 23557 zerdivemp1 24093 zerdivemp1x 28929 usgra2wlkspthlem1 30464 clwlkisclwwlklem2a4 30614 clwlkisclwwlklem2a 30615 erclwwlktr 30653 erclwwlkntr 30669 rusgrasn 30725 frgranbnb 30780 vdn0frgrav2 30784 vdn1frgrav2 30786 frgrawopreg 30810 frgrareg 30878 frgraregord013 30879 scmatsubcl 31083 scmatmulcl 31085 lindslinindsimp1 31143 ldepspr 31159 pm2mpf1 31306 mp2pm2mplem4 31316 |
Copyright terms: Public domain | W3C validator |