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  13759  fi1uzind  14465  brfi1indALT  14468  swrdswrdlem  14661  initoeu2lem1  17974  nzerooringczr  21340  pm2mpf1  22621  mp2pm2mplem4  22631  neindisj2  22947  2ndcdisj  23280  cusgrsize2inds  29143  elwwlks2  29653  clwlkclwwlklem2a4  29683  clwlkclwwlklem2a  29684  erclwwlktr  29708  erclwwlkntr  29757  clwwlknonex2lem2  29794  frgrnbnb  29979  frgrregord013  30081  zerdivemp1x  37279  icceuelpart  46563  lighneallem3  46734  bgoldbtbndlem4  46935  bgoldbtbnd  46936  tgoldbach  46944  lindslinindsimp1  47300  ldepspr  47316  nn0sumshdiglemA  47467  nn0sumshdiglemB  47468