![]() |
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 13823 addmodlteq 13984 fi1uzind 14543 brfi1indALT 14546 swrdswrdlem 14739 2cshwcshw 14861 lcmfdvdsb 16677 initoeu1 18065 initoeu2lem1 18068 initoeu2 18070 termoeu1 18072 upgrwlkdvdelem 29769 spthonepeq 29785 usgr2pthlem 29796 erclwwlktr 30051 erclwwlkntr 30100 3cyclfrgrrn1 30314 frgrnbnb 30322 frgrncvvdeqlem8 30335 frgrreg 30423 frgrregord013 30424 zerdivemp1x 37934 bgoldbtbndlem4 47733 bgoldbtbnd 47734 tgoldbach 47742 |
Copyright terms: Public domain | W3C validator |