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  13793  fi1uzind  14517  brfi1indALT  14520  swrdswrdlem  14714  initoeu2lem1  18030  nzerooringczr  21512  pm2mpf1  22839  mp2pm2mplem4  22849  neindisj2  23163  2ndcdisj  23496  cusgrsize2inds  29600  elwwlks2  30115  clwlkclwwlklem2a4  30145  clwlkclwwlklem2a  30146  erclwwlktr  30170  erclwwlkntr  30219  clwwlknonex2lem2  30256  frgrnbnb  30441  frgrregord013  30543  zerdivemp1x  38410  icceuelpart  48006  lighneallem3  48180  bgoldbtbndlem4  48394  bgoldbtbnd  48395  tgoldbach  48403  uhgrimisgrgriclem  48516  uhgrimisgrgric  48517  clnbgrgrimlem  48519  clnbgrgrim  48520  grimedg  48521  lindslinindsimp1  49043  ldepspr  49059  nn0sumshdiglemA  49205  nn0sumshdiglemB  49206