Theorem com15 101

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 100	. 2 ⊢ (𝜓 → (𝜒 → (𝜃 → (𝜏 → (𝜑 → 𝜂)))))
3	2	com4r 94	1 ⊢ (𝜏 → (𝜓 → (𝜒 → (𝜃 → (𝜑 → 𝜂)))))

Syntax hints:   → wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is referenced by:  injresinjlem  13697  addmodlteq  13860  fi1uzind  14421  brfi1indALT  14424  swrdswrdlem  14618  2cshwcshw  14739  lcmfdvdsb  16561  initoeu1  17926  initoeu2lem1  17929  initoeu2  17931  termoeu1  17933  upgrwlkdvdelem  29735  spthonepeq  29751  usgr2pthlem  29762  erclwwlktr  30023  erclwwlkntr  30072  3cyclfrgrrn1  30286  frgrnbnb  30294  frgrncvvdeqlem8  30307  frgrreg  30395  frgrregord013  30396  zerdivemp1x  38060  bgoldbtbndlem4  47970  bgoldbtbnd  47971  tgoldbach  47979