Theorem com25 100

Description: Commutation of antecedents. Swap 2nd and 5th. Deduction associated with com14 97. (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 96	. . 3 ⊢ (𝜑 → (𝜃 → (𝜒 → (𝜓 → (𝜏 → 𝜂)))))
3	2	com45 98	. 2 ⊢ (𝜑 → (𝜃 → (𝜒 → (𝜏 → (𝜓 → 𝜂)))))
4	3	com24 96	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  13821  fi1uzind  14546  brfi1indALT  14549  swrdswrdlem  14743  initoeu2lem1  18072  nzerooringczr  21611  pm2mpf1  22937  mp2pm2mplem4  22947  neindisj2  23261  2ndcdisj  23594  cusgrsize2inds  29781  elwwlks2  30296  clwlkclwwlklem2a4  30326  clwlkclwwlklem2a  30327  erclwwlktr  30351  erclwwlkntr  30400  clwwlknonex2lem2  30437  frgrnbnb  30622  frgrregord013  30724  zerdivemp1x  38576  icceuelpart  48162  lighneallem3  48336  bgoldbtbndlem4  48550  bgoldbtbnd  48551  tgoldbach  48559  uhgrimisgrgriclem  48672  uhgrimisgrgric  48673  clnbgrgrimlem  48675  clnbgrgrim  48676  grimedg  48677  lindslinindsimp1  49214  ldepspr  49230  nn0sumshdiglemA  49376  nn0sumshdiglemB  49377