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  13748  addmodlteq  13911  fi1uzind  14472  brfi1indALT  14475  swrdswrdlem  14669  2cshwcshw  14791  lcmfdvdsb  16613  initoeu1  17973  initoeu2lem1  17976  initoeu2  17978  termoeu1  17980  upgrwlkdvdelem  29666  spthonepeq  29682  usgr2pthlem  29693  erclwwlktr  29951  erclwwlkntr  30000  3cyclfrgrrn1  30214  frgrnbnb  30222  frgrncvvdeqlem8  30235  frgrreg  30323  frgrregord013  30324  zerdivemp1x  37941  bgoldbtbndlem4  47809  bgoldbtbnd  47810  tgoldbach  47818