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

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  injresinjlem  13832  addmodlteq  13996  fi1uzind  14558  brfi1indALT  14561  swrdswrdlem  14759  2cshwcshw  14882  lcmfdvdsb  16719  initoeu1  18086  initoeu2lem1  18089  initoeu2  18091  termoeu1  18093  upgrwlkdvdelem  30125  spthonepeq  30141  usgr2pthlem  30152  erclwwlktr  30416  erclwwlkntr  30465  3cyclfrgrrn1  30683  frgrnbnb  30691  frgrncvvdeqlem8  30704  frgrreg  30792  frgrregord013  30793  zerdivemp1x  38631  bgoldbtbndlem4  48606  bgoldbtbnd  48607  tgoldbach  48615