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  13755  addmodlteq  13918  fi1uzind  14479  brfi1indALT  14482  swrdswrdlem  14676  2cshwcshw  14798  lcmfdvdsb  16620  initoeu1  17980  initoeu2lem1  17983  initoeu2  17985  termoeu1  17987  upgrwlkdvdelem  29673  spthonepeq  29689  usgr2pthlem  29700  erclwwlktr  29958  erclwwlkntr  30007  3cyclfrgrrn1  30221  frgrnbnb  30229  frgrncvvdeqlem8  30242  frgrreg  30330  frgrregord013  30331  zerdivemp1x  37948  bgoldbtbndlem4  47813  bgoldbtbnd  47814  tgoldbach  47822