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  13803  fi1uzind  14525  brfi1indALT  14528  swrdswrdlem  14722  initoeu2lem1  18027  nzerooringczr  21441  pm2mpf1  22737  mp2pm2mplem4  22747  neindisj2  23061  2ndcdisj  23394  cusgrsize2inds  29433  elwwlks2  29948  clwlkclwwlklem2a4  29978  clwlkclwwlklem2a  29979  erclwwlktr  30003  erclwwlkntr  30052  clwwlknonex2lem2  30089  frgrnbnb  30274  frgrregord013  30376  zerdivemp1x  37971  icceuelpart  47450  lighneallem3  47621  bgoldbtbndlem4  47822  bgoldbtbnd  47823  tgoldbach  47831  uhgrimisgrgriclem  47943  uhgrimisgrgric  47944  clnbgrgrimlem  47946  clnbgrgrim  47947  grimedg  47948  lindslinindsimp1  48433  ldepspr  48449  nn0sumshdiglemA  48599  nn0sumshdiglemB  48600