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  12588  fi1uzind  13279  brfi1indALT  13282  fi1uzindOLD  13285  brfi1indALTOLD  13288  swrdswrdlem  13459  initoeu2lem1  16664  pm2mpf1  20604  mp2pm2mplem4  20614  neindisj2  20927  2ndcdisj  21259  cusgrsize2inds  26349  elwwlks2  26861  clwlkclwwlklem2a4  26898  clwlkclwwlklem2a  26899  erclwwlkstr  26936  erclwwlksntr  26948  frgrnbnb  27157  numclwwlkovf2exlem2  27212  frgrregord013  27253  zerdivemp1x  33746  icceuelpart  41372  lighneallem3  41524  bgoldbtbndlem4  41696  bgoldbtbnd  41697  tgoldbach  41705  tgoldbachOLD  41712  nzerooringczr  42072  lindslinindsimp1  42246  ldepspr  42262  nn0sumshdiglemA  42413  nn0sumshdiglemB  42414