Theorem com25 99

Description: Commutation of antecedents. Swap 2nd and 5th. Deduction associated with com14 96. (Contributed by Jeff Hankins, 28-Jun-2009.)

Hypothesis

Ref	Expression
com5.1	⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → (𝜏 → 𝜂)))))

Assertion

Ref	Expression
com25	⊢ (𝜑 → (𝜏 → (𝜒 → (𝜃 → (𝜓 → 𝜂)))))

Proof of Theorem com25

Step	Hyp	Ref	Expression
1		com5.1	. . . 4 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → (𝜏 → 𝜂)))))
2	1	com24 95	. . 3 ⊢ (𝜑 → (𝜃 → (𝜒 → (𝜓 → (𝜏 → 𝜂)))))
3	2	com45 97	. 2 ⊢ (𝜑 → (𝜃 → (𝜒 → (𝜏 → (𝜓 → 𝜂)))))
4	3	com24 95	1 ⊢ (𝜑 → (𝜏 → (𝜒 → (𝜃 → (𝜓 → 𝜂)))))

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  13823  fi1uzind  14543  brfi1indALT  14546  swrdswrdlem  14739  initoeu2lem1  18068  nzerooringczr  21509  pm2mpf1  22821  mp2pm2mplem4  22831  neindisj2  23147  2ndcdisj  23480  cusgrsize2inds  29486  elwwlks2  29996  clwlkclwwlklem2a4  30026  clwlkclwwlklem2a  30027  erclwwlktr  30051  erclwwlkntr  30100  clwwlknonex2lem2  30137  frgrnbnb  30322  frgrregord013  30424  zerdivemp1x  37934  icceuelpart  47361  lighneallem3  47532  bgoldbtbndlem4  47733  bgoldbtbnd  47734  tgoldbach  47742  uhgrimisgrgriclem  47836  uhgrimisgrgric  47837  clnbgrgrimlem  47839  clnbgrgrim  47840  grimedg  47841  lindslinindsimp1  48303  ldepspr  48319  nn0sumshdiglemA  48469  nn0sumshdiglemB  48470