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 13147 addmodlteq 13304 fi1uzind 13845 brfi1indALT 13848 swrdswrdlem 14056 2cshwcshw 14177 lcmfdvdsb 15977 initoeu1 17261 initoeu2lem1 17264 initoeu2 17266 termoeu1 17268 upgrwlkdvdelem 27445 spthonepeq 27461 usgr2pthlem 27472 erclwwlktr 27728 erclwwlkntr 27778 3cyclfrgrrn1 27992 frgrnbnb 28000 frgrncvvdeqlem8 28013 frgrreg 28101 frgrregord013 28102 zerdivemp1x 35108 bgoldbtbndlem4 43820 bgoldbtbnd 43821 tgoldbach 43829 |
Copyright terms: Public domain | W3C validator |