Theorem com34 86

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

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 85	. 2 |- ( ( ch -> ( th -> ta ) ) -> ( th -> ( ch -> ta ) ) )
3	1, 2	syl6 34	1 |- ( ph -> ( ps -> ( th -> ( ch -> ta ) ) ) )

Syntax hints:   -> wi 4

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

This theorem is referenced by:  com4l  87  com35  93  3an1rs  1221  ad5ant14  1244  ad5ant15  1245  ad5ant24  1247  ad5ant25  1248  ad5ant245  1249  ad5ant124  1253  ad5ant134  1255  ad5ant135  1256  ad5ant145  1257  rspct  3143  po2nr  4768  wefrc  4828  tz7.7  5449  funssres  5622  isomin  6228  f1ocnv2d  6520  onint  6622  f1oweALT  6777  bropfvvvv  6876  wfrlem12  7047  tfrlem9  7103  tz7.49  7162  oelim  7236  oaordex  7259  omordi  7267  omass  7281  oen0  7287  nnmass  7325  nnmordi  7332  inf3lem2  8134  epfrs  8215  indcardi  8472  ackbij1lem16  8665  cfcoflem  8702  axcc3  8868  zorn2lem7  8932  grur1a  9244  genpcd  9431  genpnmax  9432  mulclprlem  9444  distrlem1pr  9450  ltaddpr  9459  ltexprlem6  9466  ltexprlem7  9467  mulgt0sr  9529  divgt0  10473  divge0  10474  sup2  10565  uzind2  11028  uzwo  11222  supxrun  11601  expnbnd  12401  facdiv  12472  hashimarni  12611  swrdswrdlem  12815  wrd2ind  12834  caubnd  13421  lcmfunsnlem2lem1  14611  ncoprmlnprm  14677  cshwshashlem1  15066  psgnunilem4  17138  lmodvsdi  18114  xrsdsreclblem  19014  cpmatacl  19740  riinopn  19938  0ntr  20087  elcls  20089  hausnei2  20369  fgfil  20890  alexsubALTlem2  21063  alexsubALT  21066  aalioulem3  23290  aalioulem4  23291  wilthlem3  23995  usgra2adedgspthlem2  25340  nbhashuvtx1  25643  3cyclfrgrarn  25741  n4cyclfrgra  25746  frgraregord013  25846  grpoidinvlem3  25934  elspansn5  27227  atcv1  28033  atcvatlem  28038  chirredlem3  28045  mdsymlem3  28058  mdsymlem5  28060  mdsymlem6  28061  sumdmdlem2  28072  f1o3d  28229  slmdvsdi  28531  frrlem11  30526  fgmin  31026  nndivsub  31117  mblfinlem3  31979  rngonegrmul  32191  crngm23  32235  hlrelat2  32968  pmaple  33326  pmodlem2  33412  dalaw  33451  syl5imp  36869  com3rgbi  36871  ee223  37013  iccpartigtl  38737  iccelpart  38747  bgoldbtbndlem3  38902  upgrewlkle2  39625  upgrspths1wlklem  39696  nzerooringczr  40127  ply1mulgsumlem1  40231  fllog2  40432