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 843  po2nr 2838  wefrc 2933  tz7.7 2963  onint 2996  funssres 3538  isomin 3884  f1oweALT 3891  tfrlem9 3904  tz7.49 3944  oelim 4153  oaordex 4176  omordi 4181  omass 4195  oen0 4197  oeordi 4198  en3d 4382  inf3lem2 4586  zfregs 4619  zorn2lem7 4766  genpcd 5081  genpnmax 5082  mulclprlem 5093  ltaddpr 5112  ltexprlem6 5119  ltexprlem7 5120  prlem936b 5126  divgt0t 5809  divge0t 5810  sup2 5998  supxrun 6032  uzind2 6154  uzwo4OLD 6158  uzwo3lem1 6164  qbtwnre 6216  uzwo 6387  uzwoOLD 6388  fsequb 6455  expgt0t 6520  expgt1t 6523  divexpt 6530  expword2it 6536  expnbndt 6585  facdivt 6879  caucvglem2 7094  cvgratlem1 7185  infxpidmlem11 7505  clsval2 7627  0ntr 7644  elcls 7646  cnpco 7708  metcnp 7826  lmuni 7886  metcn4i 7906  bcthlem20 7952  bcthlem28 7960  grpidinvlem3 7984  ubthlem5 8464  ubthlem13 8472  minvecex 8509  elspansn5t 9414  atcv1t 10215  atcvatlem 10220  irredlem3 10227  mdsymlem3 10240  mdsymlem5 10242  mdsymlem6 10243  sumdmdlem2 10253  fiiu2 10377  efilcp 10445  efilcp2 10450  cmpmon 10585

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

Copyright terms: Public domain