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  13435  fi1uzind  14139  brfi1indALT  14142  swrdswrdlem  14345  initoeu2lem1  17645  pm2mpf1  21856  mp2pm2mplem4  21866  neindisj2  22182  2ndcdisj  22515  cusgrsize2inds  27723  elwwlks2  28232  clwlkclwwlklem2a4  28262  clwlkclwwlklem2a  28263  erclwwlktr  28287  erclwwlkntr  28336  clwwlknonex2lem2  28373  frgrnbnb  28558  frgrregord013  28660  zerdivemp1x  36032  icceuelpart  44776  lighneallem3  44947  bgoldbtbndlem4  45148  bgoldbtbnd  45149  tgoldbach  45157  nzerooringczr  45518  lindslinindsimp1  45686  ldepspr  45702  nn0sumshdiglemA  45853  nn0sumshdiglemB  45854