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  13826  addmodlteq  13987  fi1uzind  14546  brfi1indALT  14549  swrdswrdlem  14742  2cshwcshw  14864  lcmfdvdsb  16680  initoeu1  18056  initoeu2lem1  18059  initoeu2  18061  termoeu1  18063  upgrwlkdvdelem  29756  spthonepeq  29772  usgr2pthlem  29783  erclwwlktr  30041  erclwwlkntr  30090  3cyclfrgrrn1  30304  frgrnbnb  30312  frgrncvvdeqlem8  30325  frgrreg  30413  frgrregord013  30414  zerdivemp1x  37954  bgoldbtbndlem4  47795  bgoldbtbnd  47796  tgoldbach  47804