| 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 13826 fi1uzind 14546 brfi1indALT 14549 swrdswrdlem 14742 initoeu2lem1 18059 nzerooringczr 21491 pm2mpf1 22805 mp2pm2mplem4 22815 neindisj2 23131 2ndcdisj 23464 cusgrsize2inds 29471 elwwlks2 29986 clwlkclwwlklem2a4 30016 clwlkclwwlklem2a 30017 erclwwlktr 30041 erclwwlkntr 30090 clwwlknonex2lem2 30127 frgrnbnb 30312 frgrregord013 30414 zerdivemp1x 37954 icceuelpart 47423 lighneallem3 47594 bgoldbtbndlem4 47795 bgoldbtbnd 47796 tgoldbach 47804 uhgrimisgrgriclem 47898 uhgrimisgrgric 47899 clnbgrgrimlem 47901 clnbgrgrim 47902 grimedg 47903 lindslinindsimp1 48374 ldepspr 48390 nn0sumshdiglemA 48540 nn0sumshdiglemB 48541 |
| Copyright terms: Public domain | W3C validator |