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  13846  addmodlteq  14010  fi1uzind  14572  brfi1indALT  14575  swrdswrdlem  14773  2cshwcshw  14896  lcmfdvdsb  16733  initoeu1  18100  initoeu2lem1  18103  initoeu2  18105  termoeu1  18107  upgrwlkdvdelem  30201  spthonepeq  30217  usgr2pthlem  30228  erclwwlktr  30492  erclwwlkntr  30541  3cyclfrgrrn1  30765  frgrnbnb  30773  frgrncvvdeqlem8  30786  frgrreg  30874  frgrregord013  30875  zerdivemp1x  38697  bgoldbtbndlem4  48724  bgoldbtbnd  48725  tgoldbach  48733