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 ⊢ (𝜏 → (𝜓 → (𝜒 → (𝜃 → (𝜑 → 𝜂)))))

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  13815  addmodlteq  13978  fi1uzind  14540  brfi1indALT  14543  swrdswrdlem  14737  2cshwcshw  14858  lcmfdvdsb  16697  initoeu1  18064  initoeu2lem1  18067  initoeu2  18069  termoeu1  18071  upgrwlkdvdelem  30022  spthonepeq  30038  usgr2pthlem  30049  erclwwlktr  30310  erclwwlkntr  30359  3cyclfrgrrn1  30573  frgrnbnb  30581  frgrncvvdeqlem8  30594  frgrreg  30682  frgrregord013  30683  zerdivemp1x  38481  bgoldbtbndlem4  48457  bgoldbtbnd  48458  tgoldbach  48466