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  13152  addmodlteq  13309  fi1uzind  13851  brfi1indALT  13854  swrdswrdlem  14057  2cshwcshw  14178  lcmfdvdsb  15977  initoeu1  17263  initoeu2lem1  17266  initoeu2  17268  termoeu1  17270  upgrwlkdvdelem  27525  spthonepeq  27541  usgr2pthlem  27552  erclwwlktr  27807  erclwwlkntr  27856  3cyclfrgrrn1  28070  frgrnbnb  28078  frgrncvvdeqlem8  28091  frgrreg  28179  frgrregord013  28180  zerdivemp1x  35385  bgoldbtbndlem4  44326  bgoldbtbnd  44327  tgoldbach  44335