Theorem com23 78

Description: Commutation of antecedents. Swap 2nd and 3rd. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 4-Aug-2012.)

Hypothesis

Ref	Expression
com3.1	|- ( ph -> ( ps -> ( ch -> th ) ) )

Assertion

Ref	Expression
com23	|- ( ph -> ( ch -> ( ps -> th ) ) )

Proof of Theorem com23

Step	Hyp	Ref	Expression
1		com3.1	. 2 |- ( ph -> ( ps -> ( ch -> th ) ) )
2		pm2.27 40	. 2 |- ( ch -> ( ( ch -> th ) -> th ) )
3	1, 2	syl9 72	1 |- ( ph -> ( ch -> ( ps -> th ) ) )

Syntax hints:   -> wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is referenced by:  com3r  79  com13  80  pm2.04  82  pm2.86d  100  impcomd  255  impancom  260  a2and  558  con2d  625  impidc  859  pm2.61dc  866  3com23  1211  expcomd  1452  spimth  1749  sbiedh  1801  eqrdav  2195  necon4bbiddc  2441  ralrimdva  2577  ralrimdvva  2582  ceqsalt  2789  vtoclgft  2814  reu6  2953  sbciegft  3020  reuss2  3443  reupick  3447  reusv3  4495  ssrel  4751  ssrel2  4753  ssrelrel  4763  funssres  5300  funcnvuni  5327  fv3  5581  fvmptt  5653  funfvima2  5795  isoini  5865  isopolem  5869  f1ocnv2d  6127  f1o2ndf1  6286  nnmordi  6574  nnmord  6575  xpdom2  6890  findcard2  6950  findcard2s  6951  findcard2d  6952  findcard2sd  6953  xpfi  6993  ordiso2  7101  updjud  7148  genpcdl  7586  genpcuu  7587  distrlem5prl  7653  distrlem5pru  7654  lemul12a  8889  divgt0  8899  divge0  8900  lbreu  8972  bndndx  9248  elnnz  9336  nzadd  9378  fzind  9441  fnn0ind  9442  eqreznegel  9688  lbzbi  9690  irradd  9720  irrmul  9721  ledivge1le  9801  iccid  10000  uzsubsubfz  10122  fzrevral  10180  elfz0fzfz0  10201  fz0fzelfz0  10202  elfzmlbp  10207  elfzodifsumelfzo  10277  ssfzo12bi  10301  elfzonelfzo  10306  flqeqceilz  10410  le2sq2  10707  facdiv  10830  facwordi  10832  faclbnd  10833  cau3lem  11279  mulcn2  11477  climcau  11512  climcaucn  11516  modfsummod  11623  p1modz1  11959  dvdsdivcl  12015  ltoddhalfle  12058  halfleoddlt  12059  ndvdssub  12095  dfgcd2  12181  coprmdvds1  12259  coprmdvds  12260  coprmdvds2  12261  divgcdcoprm0  12269  cncongr1  12271  cncongr2  12272  prmfac1  12320  pcqcl  12475  dvdsprmpweqle  12506  oddprmdvds  12523  prmpwdvds  12524  infpnlem1  12528  lidrididd  13025  mulgaddcom  13276  mulginvcom  13277  imasabl  13466  lmodfopnelem1  13880  lss1d  13939  rnglidlmcl  14036  znrrg  14216  uniopn  14237  tgcnp  14445  iscnp4  14454  lmtopcnp  14486  txlm  14515  metss  14730  metcnp3  14747  logbgcd1irr  15203  gausslemma2dlem1a  15299  gausslemma2dlem2  15303  gausslemma2dlem3  15304  lgsquad2lem2  15323  2lgslem1a1  15327  2sqlem6  15361  bj-rspgt  15432