Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > com25 | Structured version Visualization version Unicode version |
Description: Commutation of antecedents. Swap 2nd and 5th. Deduction associated with com14 96. (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 95 | . . 3 |
3 | 2 | com45 97 | . 2 |
4 | 3 | com24 95 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 |
This theorem is referenced by: injresinjlem 12588 fi1uzind 13279 brfi1indALT 13282 fi1uzindOLD 13285 brfi1indALTOLD 13288 swrdswrdlem 13459 initoeu2lem1 16664 pm2mpf1 20604 mp2pm2mplem4 20614 neindisj2 20927 2ndcdisj 21259 cusgrsize2inds 26349 elwwlks2 26861 clwlkclwwlklem2a4 26898 clwlkclwwlklem2a 26899 erclwwlkstr 26936 erclwwlksntr 26948 frgrnbnb 27157 numclwwlkovf2exlem2 27212 frgrregord013 27253 zerdivemp1x 33746 icceuelpart 41372 lighneallem3 41524 bgoldbtbndlem4 41696 bgoldbtbnd 41697 tgoldbach 41705 tgoldbachOLD 41712 nzerooringczr 42072 lindslinindsimp1 42246 ldepspr 42262 nn0sumshdiglemA 42413 nn0sumshdiglemB 42414 |
Copyright terms: Public domain | W3C validator |