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  13720  addmodlteq  13883  fi1uzind  14444  brfi1indALT  14447  swrdswrdlem  14641  2cshwcshw  14762  lcmfdvdsb  16584  initoeu1  17949  initoeu2lem1  17952  initoeu2  17954  termoeu1  17956  upgrwlkdvdelem  29827  spthonepeq  29843  usgr2pthlem  29854  erclwwlktr  30115  erclwwlkntr  30164  3cyclfrgrrn1  30378  frgrnbnb  30386  frgrncvvdeqlem8  30399  frgrreg  30487  frgrregord013  30488  zerdivemp1x  38227  bgoldbtbndlem4  48197  bgoldbtbnd  48198  tgoldbach  48206