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  13156  fi1uzind  13854  brfi1indALT  13857  swrdswrdlem  14065  initoeu2lem1  17273  pm2mpf1  21406  mp2pm2mplem4  21416  neindisj2  21730  2ndcdisj  22063  cusgrsize2inds  27234  elwwlks2  27744  clwlkclwwlklem2a4  27774  clwlkclwwlklem2a  27775  erclwwlktr  27799  erclwwlkntr  27849  clwwlknonex2lem2  27886  frgrnbnb  28071  frgrregord013  28173  zerdivemp1x  35224  icceuelpart  43595  lighneallem3  43771  bgoldbtbndlem4  43972  bgoldbtbnd  43973  tgoldbach  43981  nzerooringczr  44342  lindslinindsimp1  44511  ldepspr  44527  nn0sumshdiglemA  44678  nn0sumshdiglemB  44679