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  13748  fi1uzind  14472  brfi1indALT  14475  swrdswrdlem  14669  initoeu2lem1  17976  nzerooringczr  21390  pm2mpf1  22686  mp2pm2mplem4  22696  neindisj2  23010  2ndcdisj  23343  cusgrsize2inds  29381  elwwlks2  29896  clwlkclwwlklem2a4  29926  clwlkclwwlklem2a  29927  erclwwlktr  29951  erclwwlkntr  30000  clwwlknonex2lem2  30037  frgrnbnb  30222  frgrregord013  30324  zerdivemp1x  37941  icceuelpart  47437  lighneallem3  47608  bgoldbtbndlem4  47809  bgoldbtbnd  47810  tgoldbach  47818  uhgrimisgrgriclem  47930  uhgrimisgrgric  47931  clnbgrgrimlem  47933  clnbgrgrim  47934  grimedg  47935  lindslinindsimp1  48446  ldepspr  48462  nn0sumshdiglemA  48608  nn0sumshdiglemB  48609