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  13745  fi1uzind  14469  brfi1indALT  14472  swrdswrdlem  14666  initoeu2lem1  17981  nzerooringczr  21460  pm2mpf1  22764  mp2pm2mplem4  22774  neindisj2  23088  2ndcdisj  23421  cusgrsize2inds  29522  elwwlks2  30037  clwlkclwwlklem2a4  30067  clwlkclwwlklem2a  30068  erclwwlktr  30092  erclwwlkntr  30141  clwwlknonex2lem2  30178  frgrnbnb  30363  frgrregord013  30465  zerdivemp1x  38268  icceuelpart  47896  lighneallem3  48070  bgoldbtbndlem4  48284  bgoldbtbnd  48285  tgoldbach  48293  uhgrimisgrgriclem  48406  uhgrimisgrgric  48407  clnbgrgrimlem  48409  clnbgrgrim  48410  grimedg  48411  lindslinindsimp1  48933  ldepspr  48949  nn0sumshdiglemA  49095  nn0sumshdiglemB  49096