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  13718  addmodlteq  13881  fi1uzind  14442  brfi1indALT  14445  swrdswrdlem  14639  2cshwcshw  14760  lcmfdvdsb  16582  initoeu1  17947  initoeu2lem1  17950  initoeu2  17952  termoeu1  17954  upgrwlkdvdelem  29821  spthonepeq  29837  usgr2pthlem  29848  erclwwlktr  30109  erclwwlkntr  30158  3cyclfrgrrn1  30372  frgrnbnb  30380  frgrncvvdeqlem8  30393  frgrreg  30481  frgrregord013  30482  zerdivemp1x  38195  bgoldbtbndlem4  48165  bgoldbtbnd  48166  tgoldbach  48174