Theorem com15 102

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 101	. 2 ⊢ (𝜓 → (𝜒 → (𝜃 → (𝜏 → (𝜑 → 𝜂)))))
3	2	com4r 95	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  13815  addmodlteq  13978  fi1uzind  14540  brfi1indALT  14543  swrdswrdlem  14737  2cshwcshw  14858  lcmfdvdsb  16696  initoeu1  18063  initoeu2lem1  18066  initoeu2  18068  termoeu1  18070  upgrwlkdvdelem  30085  spthonepeq  30101  usgr2pthlem  30112  erclwwlktr  30373  erclwwlkntr  30422  3cyclfrgrrn1  30636  frgrnbnb  30644  frgrncvvdeqlem8  30657  frgrreg  30745  frgrregord013  30746  zerdivemp1x  38598  bgoldbtbndlem4  48573  bgoldbtbnd  48574  tgoldbach  48582