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  13905  fi1uzind  14632  brfi1indALT  14635  swrdswrdlem  14833  initoeu2lem1  18169  nzerooringczr  21766  pm2mpf1  23097  mp2pm2mplem4  23107  neindisj2  23421  2ndcdisj  23755  cusgrsize2inds  30016  elwwlks2  30540  clwlkclwwlklem2a4  30570  clwlkclwwlklem2a  30571  erclwwlktr  30595  erclwwlkntr  30644  clwwlknonex2lem2  30681  frgrnbnb  30876  frgrregord013  30978  zerdivemp1x  38849  icceuelpart  48462  lighneallem3  48636  bgoldbtbndlem4  48850  bgoldbtbnd  48851  tgoldbach  48859  uhgrimisgrgriclem  48972  uhgrimisgrgric  48973  clnbgrgrimlem  48975  clnbgrgrim  48976  grimedg  48977  lindslinindsimp1  49513  ldepspr  49529  nn0sumshdiglemA  49675  nn0sumshdiglemB  49676