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  13965  addmodlteq  14129  fi1uzind  14693  brfi1indALT  14696  swrdswrdlem  14895  2cshwcshw  15018  lcmfdvdsb  16862  initoeu1  18236  initoeu2lem1  18239  initoeu2  18241  termoeu1  18243  upgrwlkdvdelem  30379  spthonepeq  30395  usgr2pthlem  30406  erclwwlktr  30670  erclwwlkntr  30719  3cyclfrgrrn1  30943  frgrnbnb  30951  frgrncvvdeqlem8  30964  frgrreg  31052  frgrregord013  31053  zerdivemp1x  39147  bgoldbtbndlem4  49179  bgoldbtbnd  49180  tgoldbach  49188