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  13736  addmodlteq  13899  fi1uzind  14460  brfi1indALT  14463  swrdswrdlem  14657  2cshwcshw  14778  lcmfdvdsb  16603  initoeu1  17969  initoeu2lem1  17972  initoeu2  17974  termoeu1  17976  upgrwlkdvdelem  29819  spthonepeq  29835  usgr2pthlem  29846  erclwwlktr  30107  erclwwlkntr  30156  3cyclfrgrrn1  30370  frgrnbnb  30378  frgrncvvdeqlem8  30391  frgrreg  30479  frgrregord013  30480  zerdivemp1x  38282  bgoldbtbndlem4  48296  bgoldbtbnd  48297  tgoldbach  48305