![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > com15 | Structured version Visualization version GIF version |
Description: Commutation of antecedents. Swap 1st and 5th. (Contributed by Jeff Hankins, 28-Jun-2009.) (Proof shortened by Wolf Lammen, 29-Jul-2012.) |
Ref | Expression |
---|---|
com5.1 | ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → (𝜏 → 𝜂))))) |
Ref | Expression |
---|---|
com15 | ⊢ (𝜏 → (𝜓 → (𝜒 → (𝜃 → (𝜑 → 𝜂))))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | com5.1 | . . 3 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → (𝜏 → 𝜂))))) | |
2 | 1 | com5l 100 | . 2 ⊢ (𝜓 → (𝜒 → (𝜃 → (𝜏 → (𝜑 → 𝜂))))) |
3 | 2 | com4r 94 | 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 12796 addmodlteq 12953 fi1uzind 13481 brfi1indALT 13484 swrdswrdlem 13668 2cshwcshw 13780 lcmfdvdsb 15564 initoeu1 16868 initoeu2lem1 16871 initoeu2 16873 termoeu1 16875 upgrwlkdvdelem 26867 spthonepeq 26883 usgr2pthlem 26894 erclwwlktr 27172 erclwwlkntr 27229 3cyclfrgrrn1 27467 frgrnbnb 27475 frgrncvvdeqlem8 27488 frgrreg 27593 frgrregord013 27594 zerdivemp1x 34078 bgoldbtbndlem4 42224 bgoldbtbnd 42225 tgoldbach 42233 tgoldbachOLD 42240 |
Copyright terms: Public domain | W3C validator |