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  13158  addmodlteq  13315  fi1uzind  13856  brfi1indALT  13859  swrdswrdlem  14066  2cshwcshw  14187  lcmfdvdsb  15987  initoeu1  17271  initoeu2lem1  17274  initoeu2  17276  termoeu1  17278  upgrwlkdvdelem  27517  spthonepeq  27533  usgr2pthlem  27544  erclwwlktr  27800  erclwwlkntr  27850  3cyclfrgrrn1  28064  frgrnbnb  28072  frgrncvvdeqlem8  28085  frgrreg  28173  frgrregord013  28174  zerdivemp1x  35240  bgoldbtbndlem4  43993  bgoldbtbnd  43994  tgoldbach  44002