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  13837  addmodlteq  13997  fi1uzind  14556  brfi1indALT  14559  swrdswrdlem  14752  2cshwcshw  14874  lcmfdvdsb  16690  initoeu1  18078  initoeu2lem1  18081  initoeu2  18083  termoeu1  18085  upgrwlkdvdelem  29772  spthonepeq  29788  usgr2pthlem  29799  erclwwlktr  30054  erclwwlkntr  30103  3cyclfrgrrn1  30317  frgrnbnb  30325  frgrncvvdeqlem8  30338  frgrreg  30426  frgrregord013  30427  zerdivemp1x  37907  bgoldbtbndlem4  47682  bgoldbtbnd  47683  tgoldbach  47691