Nearby theorems
|
|
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 13785 addmodlteq 13944 fi1uzind 14491 brfi1indALT 14494 swrdswrdlem 14687 2cshwcshw 14809 lcmfdvdsb 16614 initoeu1 18000 initoeu2lem1 18003 initoeu2 18005 termoeu1 18007 upgrwlkdvdelem 29563 spthonepeq 29579 usgr2pthlem 29590 erclwwlktr 29845 erclwwlkntr 29894 3cyclfrgrrn1 30108 frgrnbnb 30116 frgrncvvdeqlem8 30129 frgrreg 30217 frgrregord013 30218 zerdivemp1x 37420 bgoldbtbndlem4 47148 bgoldbtbnd 47149 tgoldbach 47157 |
| Copyright terms: Public domain | W3C validator |