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  13553  addmodlteq  13712  fi1uzind  14256  brfi1indALT  14259  swrdswrdlem  14462  2cshwcshw  14583  lcmfdvdsb  16393  initoeu1  17771  initoeu2lem1  17774  initoeu2  17776  termoeu1  17778  upgrwlkdvdelem  28149  spthonepeq  28165  usgr2pthlem  28176  erclwwlktr  28431  erclwwlkntr  28480  3cyclfrgrrn1  28694  frgrnbnb  28702  frgrncvvdeqlem8  28715  frgrreg  28803  frgrregord013  28804  zerdivemp1x  36149  bgoldbtbndlem4  45318  bgoldbtbnd  45319  tgoldbach  45327