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  1194  rspct  3063  po2nr  4650  wefrc  4710  tz7.7  4741  funssres  5455  isomin  6025  f1ocnv2d  6310  onint  6405  f1oweALT  6560  tfrlem9  6840  tz7.49  6896  oelim  6970  oaordex  6993  omordi  7001  omass  7015  oen0  7021  nnmass  7059  nnmordi  7066  inf3lem2  7831  epfrs  7947  indcardi  8207  ackbij1lem16  8400  cfcoflem  8437  axcc3  8603  zorn2lem7  8667  grur1a  8982  genpcd  9171  genpnmax  9172  mulclprlem  9184  distrlem1pr  9190  ltaddpr  9199  ltexprlem6  9206  ltexprlem7  9207  mulgt0sr  9268  divgt0  10193  divge0  10194  sup2  10282  uzind2  10730  uzwo  10913  uzwoOLD  10914  supxrun  11274  expnbnd  11989  facdiv  12059  hashimarni  12197  swrdswrdlem  12349  wrd2ind  12368  caubnd  12842  cshwshashlem1  14118  psgnunilem4  15996  lmodvsdi  16951  xrsdsreclblem  17818  riinopn  18480  0ntr  18634  elcls  18636  hausnei2  18916  fgfil  19407  alexsubALTlem2  19579  alexsubALT  19582  aalioulem3  21759  aalioulem4  21760  wilthlem3  22367  grpoidinvlem3  23628  elspansn5  24912  atcv1  25719  atcvatlem  25724  chirredlem3  25731  mdsymlem3  25744  mdsymlem5  25746  mdsymlem6  25747  sumdmdlem2  25758  f1o3d  25883  slmdvsdi  26164  wfrlem12  27664  frrlem11  27709  nndivsub  28233  mblfinlem3  28355  fgmin  28516  rngonegrmul  28683  crngm23  28727  usgra2adedgspthlem2  30229  nbhashuvtx1  30458  3cyclfrgrarn  30530  n4cyclfrgra  30535  frgraregord013  30636  ad5ant14  31002  ad5ant15  31003  ad5ant24  31005  ad5ant25  31006  ad5ant245  31007  ad5ant124  31011  ad5ant134  31013  ad5ant135  31014  ad5ant145  31015  syl5imp  31050  com3rgbi  31052  ee223  31190  hlrelat2  32769  pmaple  33127  pmodlem2  33213  dalaw  33252