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  13706  fi1uzind  14430  brfi1indALT  14433  swrdswrdlem  14627  initoeu2lem1  17938  nzerooringczr  21435  pm2mpf1  22743  mp2pm2mplem4  22753  neindisj2  23067  2ndcdisj  23400  cusgrsize2inds  29527  elwwlks2  30042  clwlkclwwlklem2a4  30072  clwlkclwwlklem2a  30073  erclwwlktr  30097  erclwwlkntr  30146  clwwlknonex2lem2  30183  frgrnbnb  30368  frgrregord013  30470  zerdivemp1x  38148  icceuelpart  47682  lighneallem3  47853  bgoldbtbndlem4  48054  bgoldbtbnd  48055  tgoldbach  48063  uhgrimisgrgriclem  48176  uhgrimisgrgric  48177  clnbgrgrimlem  48179  clnbgrgrim  48180  grimedg  48181  lindslinindsimp1  48703  ldepspr  48719  nn0sumshdiglemA  48865  nn0sumshdiglemB  48866