![]() |
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 13748 addmodlteq 13907 fi1uzind 14454 brfi1indALT 14457 swrdswrdlem 14650 2cshwcshw 14772 lcmfdvdsb 16576 initoeu1 17957 initoeu2lem1 17960 initoeu2 17962 termoeu1 17964 upgrwlkdvdelem 28982 spthonepeq 28998 usgr2pthlem 29009 erclwwlktr 29264 erclwwlkntr 29313 3cyclfrgrrn1 29527 frgrnbnb 29535 frgrncvvdeqlem8 29548 frgrreg 29636 frgrregord013 29637 zerdivemp1x 36803 bgoldbtbndlem4 46462 bgoldbtbnd 46463 tgoldbach 46471 |
Copyright terms: Public domain | W3C validator |