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  13708  addmodlteq  13871  fi1uzind  14432  brfi1indALT  14435  swrdswrdlem  14628  2cshwcshw  14750  lcmfdvdsb  16572  initoeu1  17936  initoeu2lem1  17939  initoeu2  17941  termoeu1  17943  upgrwlkdvdelem  29699  spthonepeq  29715  usgr2pthlem  29726  erclwwlktr  29984  erclwwlkntr  30033  3cyclfrgrrn1  30247  frgrnbnb  30255  frgrncvvdeqlem8  30268  frgrreg  30356  frgrregord013  30357  zerdivemp1x  37926  bgoldbtbndlem4  47793  bgoldbtbnd  47794  tgoldbach  47802