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 98 | . 2 ⊢ (𝜓 → (𝜒 → (𝜃 → (𝜏 → (𝜑 → 𝜂))))) |
3 | 2 | com4r 92 | 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 12450 addmodlteq 12607 fi1uzind 13134 brfi1indALT 13137 fi1uzindOLD 13140 brfi1indALTOLD 13143 swrdswrdlem 13311 2cshwcshw 13422 lcmfdvdsb 15194 initoeu1 16484 initoeu2lem1 16487 initoeu2 16489 termoeu1 16491 spthonepeq 26117 wlkdvspthlem 26137 erclwwlktr 26343 erclwwlkntr 26355 el2wlkonot 26396 3cyclfrgrarn1 26539 frgranbnb 26547 vdn0frgrav2 26550 frgrancvvdeqlemB 26565 usg2spot2nb 26592 numclwwlkovf2ex 26613 frgrareg 26644 frgraregord013 26645 zerdivemp1x 32916 bgoldbtbndlem4 40224 bgoldbtbnd 40225 tgoldbach 40232 tgoldbachOLD 40239 upgrwlkdvdelem 40942 spthonepeq-av 40958 usgr2pthlem 40969 erclwwlkstr 41243 erclwwlksntr 41255 3cyclfrgrrn1 41455 frgrnbnb 41463 frgrncvvdeqlemB 41477 av-numclwwlkovf2ex 41517 av-frgrareg 41548 av-frgraregord013 41549 |
Copyright terms: Public domain | W3C validator |