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  13690  fi1uzind  14414  brfi1indALT  14417  swrdswrdlem  14611  initoeu2lem1  17921  nzerooringczr  21418  pm2mpf1  22715  mp2pm2mplem4  22725  neindisj2  23039  2ndcdisj  23372  cusgrsize2inds  29433  elwwlks2  29945  clwlkclwwlklem2a4  29975  clwlkclwwlklem2a  29976  erclwwlktr  30000  erclwwlkntr  30049  clwwlknonex2lem2  30086  frgrnbnb  30271  frgrregord013  30373  zerdivemp1x  37993  icceuelpart  47473  lighneallem3  47644  bgoldbtbndlem4  47845  bgoldbtbnd  47846  tgoldbach  47854  uhgrimisgrgriclem  47967  uhgrimisgrgric  47968  clnbgrgrimlem  47970  clnbgrgrim  47971  grimedg  47972  lindslinindsimp1  48495  ldepspr  48511  nn0sumshdiglemA  48657  nn0sumshdiglemB  48658