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  13826  fi1uzind  14546  brfi1indALT  14549  swrdswrdlem  14742  initoeu2lem1  18059  nzerooringczr  21491  pm2mpf1  22805  mp2pm2mplem4  22815  neindisj2  23131  2ndcdisj  23464  cusgrsize2inds  29471  elwwlks2  29986  clwlkclwwlklem2a4  30016  clwlkclwwlklem2a  30017  erclwwlktr  30041  erclwwlkntr  30090  clwwlknonex2lem2  30127  frgrnbnb  30312  frgrregord013  30414  zerdivemp1x  37954  icceuelpart  47423  lighneallem3  47594  bgoldbtbndlem4  47795  bgoldbtbnd  47796  tgoldbach  47804  uhgrimisgrgriclem  47898  uhgrimisgrgric  47899  clnbgrgrimlem  47901  clnbgrgrim  47902  grimedg  47903  lindslinindsimp1  48374  ldepspr  48390  nn0sumshdiglemA  48540  nn0sumshdiglemB  48541