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  13718  fi1uzind  14442  brfi1indALT  14445  swrdswrdlem  14639  initoeu2lem1  17950  nzerooringczr  21447  pm2mpf1  22755  mp2pm2mplem4  22765  neindisj2  23079  2ndcdisj  23412  cusgrsize2inds  29539  elwwlks2  30054  clwlkclwwlklem2a4  30084  clwlkclwwlklem2a  30085  erclwwlktr  30109  erclwwlkntr  30158  clwwlknonex2lem2  30195  frgrnbnb  30380  frgrregord013  30482  zerdivemp1x  38195  icceuelpart  47793  lighneallem3  47964  bgoldbtbndlem4  48165  bgoldbtbnd  48166  tgoldbach  48174  uhgrimisgrgriclem  48287  uhgrimisgrgric  48288  clnbgrgrimlem  48290  clnbgrgrim  48291  grimedg  48292  lindslinindsimp1  48814  ldepspr  48830  nn0sumshdiglemA  48976  nn0sumshdiglemB  48977