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  13743  fi1uzind  14467  brfi1indALT  14470  swrdswrdlem  14664  initoeu2lem1  17979  nzerooringczr  21462  pm2mpf1  22789  mp2pm2mplem4  22799  neindisj2  23113  2ndcdisj  23446  cusgrsize2inds  29547  elwwlks2  30062  clwlkclwwlklem2a4  30092  clwlkclwwlklem2a  30093  erclwwlktr  30117  erclwwlkntr  30166  clwwlknonex2lem2  30203  frgrnbnb  30388  frgrregord013  30490  zerdivemp1x  38321  icceuelpart  47918  lighneallem3  48092  bgoldbtbndlem4  48306  bgoldbtbnd  48307  tgoldbach  48315  uhgrimisgrgriclem  48428  uhgrimisgrgric  48429  clnbgrgrimlem  48431  clnbgrgrim  48432  grimedg  48433  lindslinindsimp1  48955  ldepspr  48971  nn0sumshdiglemA  49117  nn0sumshdiglemB  49118