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  13219  fi1uzind  13920  brfi1indALT  13923  swrdswrdlem  14126  initoeu2lem1  17353  pm2mpf1  21512  mp2pm2mplem4  21522  neindisj2  21836  2ndcdisj  22169  cusgrsize2inds  27355  elwwlks2  27864  clwlkclwwlklem2a4  27894  clwlkclwwlklem2a  27895  erclwwlktr  27919  erclwwlkntr  27968  clwwlknonex2lem2  28005  frgrnbnb  28190  frgrregord013  28292  zerdivemp1x  35699  icceuelpart  44370  lighneallem3  44541  bgoldbtbndlem4  44742  bgoldbtbnd  44743  tgoldbach  44751  nzerooringczr  45112  lindslinindsimp1  45280  ldepspr  45296  nn0sumshdiglemA  45447  nn0sumshdiglemB  45448