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  13708  fi1uzind  14432  brfi1indALT  14435  swrdswrdlem  14628  initoeu2lem1  17939  nzerooringczr  21405  pm2mpf1  22702  mp2pm2mplem4  22712  neindisj2  23026  2ndcdisj  23359  cusgrsize2inds  29417  elwwlks2  29929  clwlkclwwlklem2a4  29959  clwlkclwwlklem2a  29960  erclwwlktr  29984  erclwwlkntr  30033  clwwlknonex2lem2  30070  frgrnbnb  30255  frgrregord013  30357  zerdivemp1x  37929  icceuelpart  47424  lighneallem3  47595  bgoldbtbndlem4  47796  bgoldbtbnd  47797  tgoldbach  47805  uhgrimisgrgriclem  47918  uhgrimisgrgric  47919  clnbgrgrimlem  47921  clnbgrgrim  47922  grimedg  47923  lindslinindsimp1  48446  ldepspr  48462  nn0sumshdiglemA  48608  nn0sumshdiglemB  48609