Theorem com34 83

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 82	. 2 |- ( ( ch -> ( th -> ta ) ) -> ( th -> ( ch -> ta ) ) )
3	1, 2	syl6 33	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  84  com35  90  3an1rs  1209  rspct  3189  po2nr  4803  wefrc  4863  tz7.7  4894  funssres  5618  isomin  6218  f1ocnv2d  6511  onint  6615  f1oweALT  6769  tfrlem9  7056  tz7.49  7112  oelim  7186  oaordex  7209  omordi  7217  omass  7231  oen0  7237  nnmass  7275  nnmordi  7282  inf3lem2  8049  epfrs  8165  indcardi  8425  ackbij1lem16  8618  cfcoflem  8655  axcc3  8821  zorn2lem7  8885  grur1a  9200  genpcd  9387  genpnmax  9388  mulclprlem  9400  distrlem1pr  9406  ltaddpr  9415  ltexprlem6  9422  ltexprlem7  9423  mulgt0sr  9485  divgt0  10417  divge0  10418  sup2  10506  uzind2  10962  uzwo  11155  uzwoOLD  11156  supxrun  11518  expnbnd  12277  facdiv  12347  hashimarni  12479  swrdswrdlem  12666  wrd2ind  12685  caubnd  13173  cshwshashlem1  14562  psgnunilem4  16501  lmodvsdi  17514  xrsdsreclblem  18443  cpmatacl  19195  riinopn  19395  0ntr  19550  elcls  19552  hausnei2  19832  fgfil  20354  alexsubALTlem2  20526  alexsubALT  20529  aalioulem3  22708  aalioulem4  22709  wilthlem3  23322  usgra2adedgspthlem2  24590  nbhashuvtx1  24893  3cyclfrgrarn  24991  n4cyclfrgra  24996  frgraregord013  25096  grpoidinvlem3  25186  elspansn5  26470  atcv1  27277  atcvatlem  27282  chirredlem3  27289  mdsymlem3  27302  mdsymlem5  27304  mdsymlem6  27305  sumdmdlem2  27316  f1o3d  27449  slmdvsdi  27736  wfrlem12  29330  frrlem11  29375  nndivsub  29898  mblfinlem3  30029  fgmin  30164  rngonegrmul  30331  crngm23  30375  ply1mulgsumlem1  32856  ad5ant14  33102  ad5ant15  33103  ad5ant24  33105  ad5ant25  33106  ad5ant245  33107  ad5ant124  33111  ad5ant134  33113  ad5ant135  33114  ad5ant145  33115  syl5imp  33150  com3rgbi  33152  ee223  33288  hlrelat2  35002  pmaple  35360  pmodlem2  35446  dalaw  35485