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  13850  addmodlteq  14014  fi1uzind  14576  brfi1indALT  14579  swrdswrdlem  14777  2cshwcshw  14900  lcmfdvdsb  16739  initoeu1  18106  initoeu2lem1  18109  initoeu2  18111  termoeu1  18113  upgrwlkdvdelem  30209  spthonepeq  30225  usgr2pthlem  30236  erclwwlktr  30500  erclwwlkntr  30549  3cyclfrgrrn1  30773  frgrnbnb  30781  frgrncvvdeqlem8  30794  frgrreg  30882  frgrregord013  30883  zerdivemp1x  38705  bgoldbtbndlem4  48732  bgoldbtbnd  48733  tgoldbach  48741