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  13803  addmodlteq  13964  fi1uzind  14525  brfi1indALT  14528  swrdswrdlem  14722  2cshwcshw  14844  lcmfdvdsb  16662  initoeu1  18024  initoeu2lem1  18027  initoeu2  18029  termoeu1  18031  upgrwlkdvdelem  29718  spthonepeq  29734  usgr2pthlem  29745  erclwwlktr  30003  erclwwlkntr  30052  3cyclfrgrrn1  30266  frgrnbnb  30274  frgrncvvdeqlem8  30287  frgrreg  30375  frgrregord013  30376  zerdivemp1x  37971  bgoldbtbndlem4  47822  bgoldbtbnd  47823  tgoldbach  47831