Theorem com25 100

Description: Commutation of antecedents. Swap 2nd and 5th. Deduction associated with com14 97. (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 96	. . 3 ⊢ (𝜑 → (𝜃 → (𝜒 → (𝜓 → (𝜏 → 𝜂)))))
3	2	com45 98	. 2 ⊢ (𝜑 → (𝜃 → (𝜒 → (𝜏 → (𝜓 → 𝜂)))))
4	3	com24 96	1 ⊢ (𝜑 → (𝜏 → (𝜒 → (𝜃 → (𝜓 → 𝜂)))))

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  injresinjlem  13850  fi1uzind  14576  brfi1indALT  14579  swrdswrdlem  14777  initoeu2lem1  18109  nzerooringczr  21699  pm2mpf1  23030  mp2pm2mplem4  23040  neindisj2  23354  2ndcdisj  23688  cusgrsize2inds  29921  elwwlks2  30445  clwlkclwwlklem2a4  30475  clwlkclwwlklem2a  30476  erclwwlktr  30500  erclwwlkntr  30549  clwwlknonex2lem2  30586  frgrnbnb  30781  frgrregord013  30883  zerdivemp1x  38705  icceuelpart  48344  lighneallem3  48518  bgoldbtbndlem4  48732  bgoldbtbnd  48733  tgoldbach  48741  uhgrimisgrgriclem  48854  uhgrimisgrgric  48855  clnbgrgrimlem  48857  clnbgrgrim  48858  grimedg  48859  lindslinindsimp1  49395  ldepspr  49411  nn0sumshdiglemA  49557  nn0sumshdiglemB  49558