Theorem com15 102

Description: Commutation of antecedents. Swap 1st and 5th. (Contributed by Jeff Hankins, 28-Jun-2009.) (Proof shortened by Wolf Lammen, 29-Jul-2012.)

Hypothesis

Ref	Expression
com5.1	⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → (𝜏 → 𝜂)))))

Assertion

Ref	Expression
com15	⊢ (𝜏 → (𝜓 → (𝜒 → (𝜃 → (𝜑 → 𝜂)))))

Proof of Theorem com15

Step	Hyp	Ref	Expression
1		com5.1	. . 3 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → (𝜏 → 𝜂)))))
2	1	com5l 101	. 2 ⊢ (𝜓 → (𝜒 → (𝜃 → (𝜏 → (𝜑 → 𝜂)))))
3	2	com4r 95	1 ⊢ (𝜏 → (𝜓 → (𝜒 → (𝜃 → (𝜑 → 𝜂)))))

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  injresinjlem  13918  addmodlteq  14082  fi1uzind  14645  brfi1indALT  14648  swrdswrdlem  14846  2cshwcshw  14969  lcmfdvdsb  16811  initoeu1  18179  initoeu2lem1  18182  initoeu2  18184  termoeu1  18186  upgrwlkdvdelem  30315  spthonepeq  30331  usgr2pthlem  30342  erclwwlktr  30606  erclwwlkntr  30655  3cyclfrgrrn1  30879  frgrnbnb  30887  frgrncvvdeqlem8  30900  frgrreg  30988  frgrregord013  30989  zerdivemp1x  38861  bgoldbtbndlem4  48875  bgoldbtbnd  48876  tgoldbach  48884