![]() |
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 13752 addmodlteq 13911 fi1uzind 14458 brfi1indALT 14461 swrdswrdlem 14654 2cshwcshw 14776 lcmfdvdsb 16580 initoeu1 17961 initoeu2lem1 17964 initoeu2 17966 termoeu1 17968 upgrwlkdvdelem 28993 spthonepeq 29009 usgr2pthlem 29020 erclwwlktr 29275 erclwwlkntr 29324 3cyclfrgrrn1 29538 frgrnbnb 29546 frgrncvvdeqlem8 29559 frgrreg 29647 frgrregord013 29648 zerdivemp1x 36815 bgoldbtbndlem4 46476 bgoldbtbnd 46477 tgoldbach 46485 |
Copyright terms: Public domain | W3C validator |