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  13158  fi1uzind  13856  brfi1indALT  13859  swrdswrdlem  14066  initoeu2lem1  17274  pm2mpf1  21407  mp2pm2mplem4  21417  neindisj2  21731  2ndcdisj  22064  cusgrsize2inds  27235  elwwlks2  27745  clwlkclwwlklem2a4  27775  clwlkclwwlklem2a  27776  erclwwlktr  27800  erclwwlkntr  27850  clwwlknonex2lem2  27887  frgrnbnb  28072  frgrregord013  28174  zerdivemp1x  35240  icceuelpart  43645  lighneallem3  43821  bgoldbtbndlem4  44022  bgoldbtbnd  44023  tgoldbach  44031  nzerooringczr  44392  lindslinindsimp1  44561  ldepspr  44577  nn0sumshdiglemA  44728  nn0sumshdiglemB  44729