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  13837  fi1uzind  14556  brfi1indALT  14559  swrdswrdlem  14752  initoeu2lem1  18081  nzerooringczr  21514  pm2mpf1  22826  mp2pm2mplem4  22836  neindisj2  23152  2ndcdisj  23485  cusgrsize2inds  29489  elwwlks2  29999  clwlkclwwlklem2a4  30029  clwlkclwwlklem2a  30030  erclwwlktr  30054  erclwwlkntr  30103  clwwlknonex2lem2  30140  frgrnbnb  30325  frgrregord013  30427  zerdivemp1x  37907  icceuelpart  47310  lighneallem3  47481  bgoldbtbndlem4  47682  bgoldbtbnd  47683  tgoldbach  47691  uhgrimisgrgriclem  47782  uhgrimisgrgric  47783  clnbgrgrimlem  47785  clnbgrgrim  47786  grimedg  47787  lindslinindsimp1  48186  ldepspr  48202  nn0sumshdiglemA  48353  nn0sumshdiglemB  48354