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  13706  addmodlteq  13869  fi1uzind  14430  brfi1indALT  14433  swrdswrdlem  14627  2cshwcshw  14748  lcmfdvdsb  16570  initoeu1  17935  initoeu2lem1  17938  initoeu2  17940  termoeu1  17942  upgrwlkdvdelem  29809  spthonepeq  29825  usgr2pthlem  29836  erclwwlktr  30097  erclwwlkntr  30146  3cyclfrgrrn1  30360  frgrnbnb  30368  frgrncvvdeqlem8  30381  frgrreg  30469  frgrregord013  30470  zerdivemp1x  38148  bgoldbtbndlem4  48054  bgoldbtbnd  48055  tgoldbach  48063