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  13694  fi1uzind  14418  brfi1indALT  14421  swrdswrdlem  14615  initoeu2lem1  17925  nzerooringczr  21421  pm2mpf1  22717  mp2pm2mplem4  22727  neindisj2  23041  2ndcdisj  23374  cusgrsize2inds  29436  elwwlks2  29951  clwlkclwwlklem2a4  29981  clwlkclwwlklem2a  29982  erclwwlktr  30006  erclwwlkntr  30055  clwwlknonex2lem2  30092  frgrnbnb  30277  frgrregord013  30379  zerdivemp1x  38010  icceuelpart  47563  lighneallem3  47734  bgoldbtbndlem4  47935  bgoldbtbnd  47936  tgoldbach  47944  uhgrimisgrgriclem  48057  uhgrimisgrgric  48058  clnbgrgrimlem  48060  clnbgrgrim  48061  grimedg  48062  lindslinindsimp1  48585  ldepspr  48601  nn0sumshdiglemA  48747  nn0sumshdiglemB  48748