![]() |
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 13759 fi1uzind 14465 brfi1indALT 14468 swrdswrdlem 14661 initoeu2lem1 17974 nzerooringczr 21340 pm2mpf1 22621 mp2pm2mplem4 22631 neindisj2 22947 2ndcdisj 23280 cusgrsize2inds 29143 elwwlks2 29653 clwlkclwwlklem2a4 29683 clwlkclwwlklem2a 29684 erclwwlktr 29708 erclwwlkntr 29757 clwwlknonex2lem2 29794 frgrnbnb 29979 frgrregord013 30081 zerdivemp1x 37279 icceuelpart 46563 lighneallem3 46734 bgoldbtbndlem4 46935 bgoldbtbnd 46936 tgoldbach 46944 lindslinindsimp1 47300 ldepspr 47316 nn0sumshdiglemA 47467 nn0sumshdiglemB 47468 |
Copyright terms: Public domain | W3C validator |