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  13160  addmodlteq  13317  fi1uzind  13858  brfi1indALT  13861  swrdswrdlem  14068  2cshwcshw  14189  lcmfdvdsb  15989  initoeu1  17273  initoeu2lem1  17276  initoeu2  17278  termoeu1  17280  upgrwlkdvdelem  27519  spthonepeq  27535  usgr2pthlem  27546  erclwwlktr  27802  erclwwlkntr  27852  3cyclfrgrrn1  28066  frgrnbnb  28074  frgrncvvdeqlem8  28087  frgrreg  28175  frgrregord013  28176  zerdivemp1x  35227  bgoldbtbndlem4  43980  bgoldbtbnd  43981  tgoldbach  43989