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  13507  fi1uzind  14211  brfi1indALT  14214  swrdswrdlem  14417  initoeu2lem1  17729  pm2mpf1  21948  mp2pm2mplem4  21958  neindisj2  22274  2ndcdisj  22607  cusgrsize2inds  27820  elwwlks2  28331  clwlkclwwlklem2a4  28361  clwlkclwwlklem2a  28362  erclwwlktr  28386  erclwwlkntr  28435  clwwlknonex2lem2  28472  frgrnbnb  28657  frgrregord013  28759  zerdivemp1x  36105  icceuelpart  44888  lighneallem3  45059  bgoldbtbndlem4  45260  bgoldbtbnd  45261  tgoldbach  45269  nzerooringczr  45630  lindslinindsimp1  45798  ldepspr  45814  nn0sumshdiglemA  45965  nn0sumshdiglemB  45966