Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > com25 | Structured version Visualization version GIF version |
Description: Commutation of antecedents. Swap 2nd and 5th. Deduction associated with com14 96. (Contributed by Jeff Hankins, 28-Jun-2009.) |
Ref | Expression |
---|---|
com5.1 | ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → (𝜏 → 𝜂))))) |
Ref | Expression |
---|---|
com25 | ⊢ (𝜑 → (𝜏 → (𝜒 → (𝜃 → (𝜓 → 𝜂))))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | com5.1 | . . . 4 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → (𝜏 → 𝜂))))) | |
2 | 1 | com24 95 | . . 3 ⊢ (𝜑 → (𝜃 → (𝜒 → (𝜓 → (𝜏 → 𝜂))))) |
3 | 2 | com45 97 | . 2 ⊢ (𝜑 → (𝜃 → (𝜒 → (𝜏 → (𝜓 → 𝜂))))) |
4 | 3 | com24 95 | 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 13147 fi1uzind 13845 brfi1indALT 13848 swrdswrdlem 14056 initoeu2lem1 17264 pm2mpf1 21337 mp2pm2mplem4 21347 neindisj2 21661 2ndcdisj 21994 cusgrsize2inds 27163 elwwlks2 27673 clwlkclwwlklem2a4 27703 clwlkclwwlklem2a 27704 erclwwlktr 27728 erclwwlkntr 27778 clwwlknonex2lem2 27815 frgrnbnb 28000 frgrregord013 28102 zerdivemp1x 35108 icceuelpart 43443 lighneallem3 43619 bgoldbtbndlem4 43820 bgoldbtbnd 43821 tgoldbach 43829 nzerooringczr 44241 lindslinindsimp1 44410 ldepspr 44426 nn0sumshdiglemA 44577 nn0sumshdiglemB 44578 |
Copyright terms: Public domain | W3C validator |