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  13745  addmodlteq  13908  fi1uzind  14469  brfi1indALT  14472  swrdswrdlem  14666  2cshwcshw  14787  lcmfdvdsb  16612  initoeu1  17978  initoeu2lem1  17981  initoeu2  17983  termoeu1  17985  upgrwlkdvdelem  29804  spthonepeq  29820  usgr2pthlem  29831  erclwwlktr  30092  erclwwlkntr  30141  3cyclfrgrrn1  30355  frgrnbnb  30363  frgrncvvdeqlem8  30376  frgrreg  30464  frgrregord013  30465  zerdivemp1x  38268  bgoldbtbndlem4  48284  bgoldbtbnd  48285  tgoldbach  48293