![]() |
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 13793 addmodlteq 13952 fi1uzind 14502 brfi1indALT 14505 swrdswrdlem 14698 2cshwcshw 14820 lcmfdvdsb 16630 initoeu1 18019 initoeu2lem1 18022 initoeu2 18024 termoeu1 18026 upgrwlkdvdelem 29642 spthonepeq 29658 usgr2pthlem 29669 erclwwlktr 29924 erclwwlkntr 29973 3cyclfrgrrn1 30187 frgrnbnb 30195 frgrncvvdeqlem8 30208 frgrreg 30296 frgrregord013 30297 zerdivemp1x 37571 bgoldbtbndlem4 47290 bgoldbtbnd 47291 tgoldbach 47299 |
Copyright terms: Public domain | W3C validator |