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 ⊢ (𝜑 → (𝜏 → (𝜒 → (𝜃 → (𝜓 → 𝜂)))))

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  injresinjlem  13838  fi1uzind  14564  brfi1indALT  14567  swrdswrdlem  14765  initoeu2lem1  18096  nzerooringczr  21667  pm2mpf1  22993  mp2pm2mplem4  23003  neindisj2  23317  2ndcdisj  23650  cusgrsize2inds  29840  elwwlks2  30355  clwlkclwwlklem2a4  30385  clwlkclwwlklem2a  30386  erclwwlktr  30410  erclwwlkntr  30459  clwwlknonex2lem2  30496  frgrnbnb  30681  frgrregord013  30783  zerdivemp1x  38639  icceuelpart  48226  lighneallem3  48400  bgoldbtbndlem4  48614  bgoldbtbnd  48615  tgoldbach  48623  uhgrimisgrgriclem  48736  uhgrimisgrgric  48737  clnbgrgrimlem  48739  clnbgrgrim  48740  grimedg  48741  lindslinindsimp1  49278  ldepspr  49294  nn0sumshdiglemA  49440  nn0sumshdiglemB  49441