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  13952  fi1uzind  14679  brfi1indALT  14682  swrdswrdlem  14881  initoeu2lem1  18218  nzerooringczr  21816  pm2mpf1  23147  mp2pm2mplem4  23157  neindisj2  23471  2ndcdisj  23805  cusgrsize2inds  30064  elwwlks2  30588  clwlkclwwlklem2a4  30618  clwlkclwwlklem2a  30619  erclwwlktr  30643  erclwwlkntr  30692  clwwlknonex2lem2  30729  frgrnbnb  30924  frgrregord013  31026  zerdivemp1x  39073  icceuelpart  48723  lighneallem3  48897  bgoldbtbndlem4  49111  bgoldbtbnd  49112  tgoldbach  49120  uhgrimisgrgriclem  49233  uhgrimisgrgric  49234  clnbgrgrimlem  49236  clnbgrgrim  49237  grimedg  49238  lindslinindsimp1  49774  ldepspr  49790  nn0sumshdiglemA  49936  nn0sumshdiglemB  49937