![]() |
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 12911 addmodlteq 13068 fi1uzind 13597 brfi1indALT 13600 swrdswrdlem 13817 2cshwcshw 13980 lcmfdvdsb 15766 initoeu1 17050 initoeu2lem1 17053 initoeu2 17055 termoeu1 17057 upgrwlkdvdelem 27092 spthonepeq 27108 usgr2pthlem 27119 erclwwlktr 27415 erclwwlkntr 27473 3cyclfrgrrn1 27697 frgrnbnb 27705 frgrncvvdeqlem8 27718 frgrreg 27830 frgrregord013 27831 zerdivemp1x 34375 bgoldbtbndlem4 42731 bgoldbtbnd 42732 tgoldbach 42740 |
Copyright terms: Public domain | W3C validator |