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  13685  addmodlteq  13848  fi1uzind  14409  brfi1indALT  14412  swrdswrdlem  14606  2cshwcshw  14727  lcmfdvdsb  16549  initoeu1  17913  initoeu2lem1  17916  initoeu2  17918  termoeu1  17920  upgrwlkdvdelem  29709  spthonepeq  29725  usgr2pthlem  29736  erclwwlktr  29994  erclwwlkntr  30043  3cyclfrgrrn1  30257  frgrnbnb  30265  frgrncvvdeqlem8  30278  frgrreg  30366  frgrregord013  30367  zerdivemp1x  37987  bgoldbtbndlem4  47839  bgoldbtbnd  47840  tgoldbach  47848