![]() |
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 13011 fi1uzind 13705 brfi1indALT 13708 swrdswrdlem 13906 initoeu2lem1 17107 pm2mpf1 21095 mp2pm2mplem4 21105 neindisj2 21419 2ndcdisj 21752 cusgrsize2inds 26922 elwwlks2 27431 clwlkclwwlklem2a4 27461 clwlkclwwlklem2a 27462 erclwwlktr 27486 erclwwlkntr 27536 clwwlknonex2lem2 27573 frgrnbnb 27760 frgrregord013 27862 zerdivemp1x 34778 icceuelpart 43100 lighneallem3 43276 bgoldbtbndlem4 43477 bgoldbtbnd 43478 tgoldbach 43486 nzerooringczr 43843 lindslinindsimp1 44014 ldepspr 44030 nn0sumshdiglemA 44182 nn0sumshdiglemB 44183 |
Copyright terms: Public domain | W3C validator |