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  13736  fi1uzind  14460  brfi1indALT  14463  swrdswrdlem  14657  initoeu2lem1  17972  nzerooringczr  21470  pm2mpf1  22774  mp2pm2mplem4  22784  neindisj2  23098  2ndcdisj  23431  cusgrsize2inds  29537  elwwlks2  30052  clwlkclwwlklem2a4  30082  clwlkclwwlklem2a  30083  erclwwlktr  30107  erclwwlkntr  30156  clwwlknonex2lem2  30193  frgrnbnb  30378  frgrregord013  30480  zerdivemp1x  38282  icceuelpart  47908  lighneallem3  48082  bgoldbtbndlem4  48296  bgoldbtbnd  48297  tgoldbach  48305  uhgrimisgrgriclem  48418  uhgrimisgrgric  48419  clnbgrgrimlem  48421  clnbgrgrim  48422  grimedg  48423  lindslinindsimp1  48945  ldepspr  48961  nn0sumshdiglemA  49107  nn0sumshdiglemB  49108