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  13580  addmodlteq  13739  fi1uzind  14283  brfi1indALT  14286  swrdswrdlem  14489  2cshwcshw  14610  lcmfdvdsb  16418  initoeu1  17796  initoeu2lem1  17799  initoeu2  17801  termoeu1  17803  upgrwlkdvdelem  28213  spthonepeq  28229  usgr2pthlem  28240  erclwwlktr  28495  erclwwlkntr  28544  3cyclfrgrrn1  28758  frgrnbnb  28766  frgrncvvdeqlem8  28779  frgrreg  28867  frgrregord013  28868  zerdivemp1x  36161  bgoldbtbndlem4  45512  bgoldbtbnd  45513  tgoldbach  45521