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 31	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  3152  po2nr  4756  wefrc  4816  tz7.7  5435  funssres  5608  isomin  6215  f1ocnv2d  6506  onint  6612  f1oweALT  6767  wfrlem12  7031  tfrlem9  7087  tz7.49  7146  oelim  7220  oaordex  7243  omordi  7251  omass  7265  oen0  7271  nnmass  7309  nnmordi  7316  inf3lem2  8078  epfrs  8193  indcardi  8453  ackbij1lem16  8646  cfcoflem  8683  axcc3  8849  zorn2lem7  8913  grur1a  9226  genpcd  9413  genpnmax  9414  mulclprlem  9426  distrlem1pr  9432  ltaddpr  9441  ltexprlem6  9448  ltexprlem7  9449  mulgt0sr  9511  divgt0  10450  divge0  10451  sup2  10538  uzind2  10995  uzwo  11189  supxrun  11559  expnbnd  12337  facdiv  12407  hashimarni  12544  swrdswrdlem  12738  wrd2ind  12757  caubnd  13338  cshwshashlem1  14787  psgnunilem4  16844  lmodvsdi  17853  xrsdsreclblem  18782  cpmatacl  19507  riinopn  19707  0ntr  19863  elcls  19865  hausnei2  20145  fgfil  20666  alexsubALTlem2  20838  alexsubALT  20841  aalioulem3  23020  aalioulem4  23021  wilthlem3  23723  usgra2adedgspthlem2  25016  nbhashuvtx1  25319  3cyclfrgrarn  25417  n4cyclfrgra  25422  frgraregord013  25522  grpoidinvlem3  25608  elspansn5  26892  atcv1  27698  atcvatlem  27703  chirredlem3  27710  mdsymlem3  27723  mdsymlem5  27725  mdsymlem6  27726  sumdmdlem2  27737  f1o3d  27898  slmdvsdi  28196  frrlem11  30086  fgmin  30585  nndivsub  30676  mblfinlem3  31405  rngonegrmul  31617  crngm23  31661  hlrelat2  32400  pmaple  32758  pmodlem2  32844  dalaw  32883  ad5ant14  36231  ad5ant15  36232  ad5ant24  36234  ad5ant25  36235  ad5ant245  36236  ad5ant124  36240  ad5ant134  36242  ad5ant135  36243  ad5ant145  36244  syl5imp  36279  com3rgbi  36281  ee223  36424  iccpartigtl  37671  iccelpart  37681  bgoldbtbndlem3  37836  nzerooringczr  38372  ply1mulgsumlem1  38478  fllog2  38680