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  13755  fi1uzind  14479  brfi1indALT  14482  swrdswrdlem  14676  initoeu2lem1  17983  nzerooringczr  21397  pm2mpf1  22693  mp2pm2mplem4  22703  neindisj2  23017  2ndcdisj  23350  cusgrsize2inds  29388  elwwlks2  29903  clwlkclwwlklem2a4  29933  clwlkclwwlklem2a  29934  erclwwlktr  29958  erclwwlkntr  30007  clwwlknonex2lem2  30044  frgrnbnb  30229  frgrregord013  30331  zerdivemp1x  37948  icceuelpart  47441  lighneallem3  47612  bgoldbtbndlem4  47813  bgoldbtbnd  47814  tgoldbach  47822  uhgrimisgrgriclem  47934  uhgrimisgrgric  47935  clnbgrgrimlem  47937  clnbgrgrim  47938  grimedg  47939  lindslinindsimp1  48450  ldepspr  48466  nn0sumshdiglemA  48612  nn0sumshdiglemB  48613