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  13790  addmodlteq  13953  fi1uzind  14514  brfi1indALT  14517  swrdswrdlem  14711  2cshwcshw  14832  lcmfdvdsb  16668  initoeu1  18035  initoeu2lem1  18038  initoeu2  18040  termoeu1  18042  upgrwlkdvdelem  29893  spthonepeq  29909  usgr2pthlem  29920  erclwwlktr  30181  erclwwlkntr  30230  3cyclfrgrrn1  30444  frgrnbnb  30452  frgrncvvdeqlem8  30465  frgrreg  30553  frgrregord013  30554  zerdivemp1x  38407  bgoldbtbndlem4  48391  bgoldbtbnd  48392  tgoldbach  48400