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  13928  fi1uzind  14655  brfi1indALT  14658  swrdswrdlem  14857  initoeu2lem1  18194  nzerooringczr  21791  pm2mpf1  23122  mp2pm2mplem4  23132  neindisj2  23446  2ndcdisj  23780  cusgrsize2inds  30039  elwwlks2  30563  clwlkclwwlklem2a4  30593  clwlkclwwlklem2a  30594  erclwwlktr  30618  erclwwlkntr  30667  clwwlknonex2lem2  30704  frgrnbnb  30899  frgrregord013  31001  zerdivemp1x  38974  icceuelpart  48611  lighneallem3  48785  bgoldbtbndlem4  48999  bgoldbtbnd  49000  tgoldbach  49008  uhgrimisgrgriclem  49121  uhgrimisgrgric  49122  clnbgrgrimlem  49124  clnbgrgrim  49125  grimedg  49126  lindslinindsimp1  49662  ldepspr  49678  nn0sumshdiglemA  49824  nn0sumshdiglemB  49825