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  13011  fi1uzind  13705  brfi1indALT  13708  swrdswrdlem  13906  initoeu2lem1  17107  pm2mpf1  21095  mp2pm2mplem4  21105  neindisj2  21419  2ndcdisj  21752  cusgrsize2inds  26922  elwwlks2  27431  clwlkclwwlklem2a4  27461  clwlkclwwlklem2a  27462  erclwwlktr  27486  erclwwlkntr  27536  clwwlknonex2lem2  27573  frgrnbnb  27760  frgrregord013  27862  zerdivemp1x  34778  icceuelpart  43100  lighneallem3  43276  bgoldbtbndlem4  43477  bgoldbtbnd  43478  tgoldbach  43486  nzerooringczr  43843  lindslinindsimp1  44014  ldepspr  44030  nn0sumshdiglemA  44182  nn0sumshdiglemB  44183