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  13930  addmodlteq  14094  fi1uzind  14657  brfi1indALT  14660  swrdswrdlem  14859  2cshwcshw  14982  lcmfdvdsb  16825  initoeu1  18193  initoeu2lem1  18196  initoeu2  18198  termoeu1  18200  upgrwlkdvdelem  30329  spthonepeq  30345  usgr2pthlem  30356  erclwwlktr  30620  erclwwlkntr  30669  3cyclfrgrrn1  30893  frgrnbnb  30901  frgrncvvdeqlem8  30914  frgrreg  31002  frgrregord013  31003  zerdivemp1x  38988  bgoldbtbndlem4  49013  bgoldbtbnd  49014  tgoldbach  49022