Theorem com15 101

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 100	. 2 ⊢ (𝜓 → (𝜒 → (𝜃 → (𝜏 → (𝜑 → 𝜂)))))
3	2	com4r 94	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  13488  addmodlteq  13647  fi1uzind  14192  brfi1indALT  14195  swrdswrdlem  14398  2cshwcshw  14519  lcmfdvdsb  16329  initoeu1  17707  initoeu2lem1  17710  initoeu2  17712  termoeu1  17714  upgrwlkdvdelem  28083  spthonepeq  28099  usgr2pthlem  28110  erclwwlktr  28365  erclwwlkntr  28414  3cyclfrgrrn1  28628  frgrnbnb  28636  frgrncvvdeqlem8  28649  frgrreg  28737  frgrregord013  28738  zerdivemp1x  36084  bgoldbtbndlem4  45212  bgoldbtbnd  45213  tgoldbach  45221