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	|- ( ph -> ( ps -> ( ch -> ( th -> ( ta -> et ) ) ) ) )

Assertion

Ref	Expression
com15	|- ( ta -> ( ps -> ( ch -> ( th -> ( ph -> et ) ) ) ) )

Proof of Theorem com15

Step	Hyp	Ref	Expression
1		com5.1	. . 3 |- ( ph -> ( ps -> ( ch -> ( th -> ( ta -> et ) ) ) ) )
2	1	com5l 100	. 2 |- ( ps -> ( ch -> ( th -> ( ta -> ( ph -> et ) ) ) ) )
3	2	com4r 94	1 |- ( ta -> ( ps -> ( ch -> ( th -> ( ph -> et ) ) ) ) )

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  12588  addmodlteq  12745  fi1uzind  13279  brfi1indALT  13282  fi1uzindOLD  13285  brfi1indALTOLD  13288  swrdswrdlem  13459  2cshwcshw  13571  lcmfdvdsb  15356  initoeu1  16661  initoeu2lem1  16664  initoeu2  16666  termoeu1  16668  upgrwlkdvdelem  26632  spthonepeq  26648  usgr2pthlem  26659  erclwwlkstr  26936  erclwwlksntr  26948  3cyclfrgrrn1  27149  frgrnbnb  27157  frgrncvvdeqlem8  27170  frgrreg  27252  frgrregord013  27253  zerdivemp1x  33746  bgoldbtbndlem4  41696  bgoldbtbnd  41697  tgoldbach  41705  tgoldbachOLD  41712