Theorem com34 83

Description: Commutation of antecedents. Swap 3rd and 4th. (Contributed by NM, 25-Apr-1994.)

Hypothesis

Ref	Expression
com4.1

Assertion

Ref	Expression
com34

Proof of Theorem com34

Step	Hyp	Ref	Expression
1		com4.1	. 2
2		pm2.04 82	. 2
3	1, 2	syl6 33	1

Syntax hints:  ->wi 4

This theorem is referenced by:  com4l  84  com35  90  3an1rs  1208  rspct  3203  po2nr  4818  wefrc  4878  tz7.7  4909  funssres  5633  isomin  6233  f1ocnv2d  6526  onint  6630  f1oweALT  6784  tfrlem9  7073  tz7.49  7129  oelim  7203  oaordex  7226  omordi  7234  omass  7248  oen0  7254  nnmass  7292  nnmordi  7299  inf3lem2  8067  epfrs  8183  indcardi  8443  ackbij1lem16  8636  cfcoflem  8673  axcc3  8839  zorn2lem7  8903  grur1a  9218  genpcd  9405  genpnmax  9406  mulclprlem  9418  distrlem1pr  9424  ltaddpr  9433  ltexprlem6  9440  ltexprlem7  9441  mulgt0sr  9503  divgt0  10435  divge0  10436  sup2  10524  uzind2  10980  uzwo  11173  uzwoOLD  11174  supxrun  11536  expnbnd  12295  facdiv  12365  hashimarni  12497  swrdswrdlem  12684  wrd2ind  12703  caubnd  13191  cshwshashlem1  14580  psgnunilem4  16522  lmodvsdi  17535  xrsdsreclblem  18464  cpmatacl  19217  riinopn  19417  0ntr  19572  elcls  19574  hausnei2  19854  fgfil  20376  alexsubALTlem2  20548  alexsubALT  20551  aalioulem3  22730  aalioulem4  22731  wilthlem3  23344  usgra2adedgspthlem2  24612  nbhashuvtx1  24915  3cyclfrgrarn  25013  n4cyclfrgra  25018  frgraregord013  25118  grpoidinvlem3  25208  elspansn5  26492  atcv1  27299  atcvatlem  27304  chirredlem3  27311  mdsymlem3  27324  mdsymlem5  27326  mdsymlem6  27327  sumdmdlem2  27338  f1o3d  27471  slmdvsdi  27758  wfrlem12  29354  frrlem11  29399  nndivsub  29922  mblfinlem3  30053  fgmin  30188  rngonegrmul  30355  crngm23  30399  nzerooringczr  32880  ply1mulgsumlem1  32986  ad5ant14  33234  ad5ant15  33235  ad5ant24  33237  ad5ant25  33238  ad5ant245  33239  ad5ant124  33243  ad5ant134  33245  ad5ant135  33246  ad5ant145  33247  syl5imp  33282  com3rgbi  33284  ee223  33420  hlrelat2  35127  pmaple  35485  pmodlem2  35571  dalaw  35610

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