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  13810  fi1uzind  14534  brfi1indALT  14537  swrdswrdlem  14731  initoeu2lem1  18061  nzerooringczr  21590  pm2mpf1  22917  mp2pm2mplem4  22927  neindisj2  23241  2ndcdisj  23574  cusgrsize2inds  29712  elwwlks2  30227  clwlkclwwlklem2a4  30257  clwlkclwwlklem2a  30258  erclwwlktr  30282  erclwwlkntr  30331  clwwlknonex2lem2  30368  frgrnbnb  30553  frgrregord013  30655  zerdivemp1x  38458  icceuelpart  48040  lighneallem3  48214  bgoldbtbndlem4  48428  bgoldbtbnd  48429  tgoldbach  48437  uhgrimisgrgriclem  48550  uhgrimisgrgric  48551  clnbgrgrimlem  48553  clnbgrgrim  48554  grimedg  48555  lindslinindsimp1  49088  ldepspr  49104  nn0sumshdiglemA  49250  nn0sumshdiglemB  49251