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  1208  rspct  3207  po2nr  4813  wefrc  4873  tz7.7  4904  funssres  5626  isomin  6219  f1ocnv2d  6508  onint  6608  f1oweALT  6765  tfrlem9  7051  tz7.49  7107  oelim  7181  oaordex  7204  omordi  7212  omass  7226  oen0  7232  nnmass  7270  nnmordi  7277  inf3lem2  8042  epfrs  8158  indcardi  8418  ackbij1lem16  8611  cfcoflem  8648  axcc3  8814  zorn2lem7  8878  grur1a  9193  genpcd  9380  genpnmax  9381  mulclprlem  9393  distrlem1pr  9399  ltaddpr  9408  ltexprlem6  9415  ltexprlem7  9416  mulgt0sr  9478  divgt0  10406  divge0  10407  sup2  10495  uzind2  10949  uzwo  11140  uzwoOLD  11141  supxrun  11503  expnbnd  12259  facdiv  12329  hashimarni  12459  swrdswrdlem  12643  wrd2ind  12662  caubnd  13150  cshwshashlem1  14434  psgnunilem4  16318  lmodvsdi  17318  xrsdsreclblem  18232  cpmatacl  18984  riinopn  19184  0ntr  19338  elcls  19340  hausnei2  19620  fgfil  20111  alexsubALTlem2  20283  alexsubALT  20286  aalioulem3  22464  aalioulem4  22465  wilthlem3  23072  usgra2adedgspthlem2  24288  nbhashuvtx1  24591  3cyclfrgrarn  24689  n4cyclfrgra  24694  frgraregord013  24795  grpoidinvlem3  24884  elspansn5  26168  atcv1  26975  atcvatlem  26980  chirredlem3  26987  mdsymlem3  27000  mdsymlem5  27002  mdsymlem6  27003  sumdmdlem2  27014  f1o3d  27144  slmdvsdi  27420  wfrlem12  28931  frrlem11  28976  nndivsub  29499  mblfinlem3  29630  fgmin  29791  rngonegrmul  29958  crngm23  30002  ply1mulgsumlem1  32059  ad5ant14  32313  ad5ant15  32314  ad5ant24  32316  ad5ant25  32317  ad5ant245  32318  ad5ant124  32322  ad5ant134  32324  ad5ant135  32325  ad5ant145  32326  syl5imp  32361  com3rgbi  32363  ee223  32500  hlrelat2  34199  pmaple  34557  pmodlem2  34643  dalaw  34682