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  1199  rspct  3081  po2nr  4669  wefrc  4729  tz7.7  4760  funssres  5473  isomin  6043  f1ocnv2d  6326  onint  6421  f1oweALT  6576  tfrlem9  6859  tz7.49  6915  oelim  6989  oaordex  7012  omordi  7020  omass  7034  oen0  7040  nnmass  7078  nnmordi  7085  inf3lem2  7850  epfrs  7966  indcardi  8226  ackbij1lem16  8419  cfcoflem  8456  axcc3  8622  zorn2lem7  8686  grur1a  9001  genpcd  9190  genpnmax  9191  mulclprlem  9203  distrlem1pr  9209  ltaddpr  9218  ltexprlem6  9225  ltexprlem7  9226  mulgt0sr  9287  divgt0  10212  divge0  10213  sup2  10301  uzind2  10749  uzwo  10932  uzwoOLD  10933  supxrun  11293  expnbnd  12008  facdiv  12078  hashimarni  12216  swrdswrdlem  12368  wrd2ind  12387  caubnd  12861  cshwshashlem1  14137  psgnunilem4  16018  lmodvsdi  16986  xrsdsreclblem  17874  riinopn  18536  0ntr  18690  elcls  18692  hausnei2  18972  fgfil  19463  alexsubALTlem2  19635  alexsubALT  19638  aalioulem3  21815  aalioulem4  21816  wilthlem3  22423  grpoidinvlem3  23708  elspansn5  24992  atcv1  25799  atcvatlem  25804  chirredlem3  25811  mdsymlem3  25824  mdsymlem5  25826  mdsymlem6  25827  sumdmdlem2  25838  f1o3d  25963  slmdvsdi  26246  wfrlem12  27750  frrlem11  27795  nndivsub  28318  mblfinlem3  28449  fgmin  28610  rngonegrmul  28777  crngm23  28821  usgra2adedgspthlem2  30323  nbhashuvtx1  30552  3cyclfrgrarn  30624  n4cyclfrgra  30629  frgraregord013  30730  ply1mulgsumlem1  30863  ad5ant14  31188  ad5ant15  31189  ad5ant24  31191  ad5ant25  31192  ad5ant245  31193  ad5ant124  31197  ad5ant134  31199  ad5ant135  31200  ad5ant145  31201  syl5imp  31236  com3rgbi  31238  ee223  31375  hlrelat2  33066  pmaple  33424  pmodlem2  33510  dalaw  33549