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  13754  fi1uzind  14460  brfi1indALT  14463  swrdswrdlem  14656  initoeu2lem1  17966  pm2mpf1  22308  mp2pm2mplem4  22318  neindisj2  22634  2ndcdisj  22967  cusgrsize2inds  28748  elwwlks2  29258  clwlkclwwlklem2a4  29288  clwlkclwwlklem2a  29289  erclwwlktr  29313  erclwwlkntr  29362  clwwlknonex2lem2  29399  frgrnbnb  29584  frgrregord013  29686  zerdivemp1x  36907  icceuelpart  46189  lighneallem3  46360  bgoldbtbndlem4  46561  bgoldbtbnd  46562  tgoldbach  46570  nzerooringczr  47055  lindslinindsimp1  47222  ldepspr  47238  nn0sumshdiglemA  47389  nn0sumshdiglemB  47390