Theorem com34 36

Description: Commutation of antecedents. Swap 3rd and 4th.

Hypothesis

Ref	Expression
com4.1	|- (ph -> (ps -> (ch -> (th -> ta))))

Assertion

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

Proof of Theorem com34

Step	Hyp	Ref	Expression
1		com4.1	. 2 |- (ph -> (ps -> (ch -> (th -> ta))))
2		pm2.04 30	. 2 |- ((ch -> (th -> ta)) -> (th -> (ch -> ta)))
3	1, 2	syl6 22	1 |- (ph -> (ps -> (th -> (ch -> ta))))

Syntax hints:   -> wi 3

This theorem is referenced by:  com24 37  com14 38  3an1rs 845  po2nr 2847  wefrc 2943  tz7.7 2973  onint 3006  funssres 3552  isomin 3899  f1oweALT 3906  tfrlem9 3919  tz7.49 3959  oelim 4169  oaordex 4192  omordi 4197  omass 4211  oen0 4213  oeordi 4214  en3d 4401  inf3lem2 4614  zfregs 4647  zorn2lem7 4794  genpcd 5109  genpnmax 5110  mulclprlem 5121  ltaddpr 5140  ltexprlem6 5147  ltexprlem7 5148  prlem936b 5154  divgt0t 5855  divge0t 5856  sup2 6051  supxrun 6085  uzind2 6206  uzwo4OLD 6210  uzwo3lem1 6216  qbtwnre 6278  ioojoint 6416  uzwo 6455  uzwoOLD 6456  fsequb 6523  expgt0t 6589  expgt1t 6592  divexpt 6599  expword2it 6605  expnbndt 6654  facdivt 6942  caucvglem2 7158  cvgratlem1 7250  infxpidmlem11 7562  clsval2 7685  0ntr 7702  elcls 7704  cnpco 7769  metcnp 7887  lmuni 7951  metcn4i 7972  bcthlem20 8018  bcthlem28 8026  grpidinvlem3 8050  nvcnpi3 8422  ubthlem5 8533  ubthlem13 8541  minvecex 8578  elspansn5t 9497  atcv1t 10307  atcvatlem 10312  irredlem3 10319  mdsymlem3 10332  mdsymlem5 10334  mdsymlem6 10335  sumdmdlem2 10346  nndivsub 10421  fiiu2 10488  fiiu2OLD 10489  efilcp 10572  efilcpOLD 10573  efilcp2 10581  efilcp2OLD 10582  cmpmon 10743

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-mp 7

Copyright terms: Public domain