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  860  pm2.61dc  867  3com23  1212  expcomd  1462  spimth  1759  sbiedh  1811  eqrdav  2206  necon4bbiddc  2452  ralrimdva  2588  ralrimdvva  2593  ceqsalt  2803  vtoclgft  2828  reu6  2969  sbciegft  3036  reuss2  3461  reupick  3465  reusv3  4525  ssrel  4781  ssrel2  4783  ssrelrel  4793  ssrelrn  4888  funssres  5332  funcnvuni  5362  fv3  5622  fvmptt  5694  funfvima2  5840  isoini  5910  isopolem  5914  f1ocnv2d  6173  f1o2ndf1  6337  nnmordi  6625  nnmord  6626  xpdom2  6951  findcard2  7012  findcard2s  7013  findcard2d  7014  findcard2sd  7015  xpfi  7055  ordiso2  7163  updjud  7210  genpcdl  7667  genpcuu  7668  distrlem5prl  7734  distrlem5pru  7735  lemul12a  8970  divgt0  8980  divge0  8981  lbreu  9053  bndndx  9329  elnnz  9417  nzadd  9460  fzind  9523  fnn0ind  9524  eqreznegel  9770  lbzbi  9772  irradd  9802  irrmul  9803  ledivge1le  9883  iccid  10082  uzsubsubfz  10204  fzrevral  10262  elfz0fzfz0  10283  fz0fzelfz0  10284  elfzmlbp  10289  elincfzoext  10359  elfzodifsumelfzo  10367  ssfzo12bi  10391  elfzonelfzo  10396  flqeqceilz  10500  le2sq2  10797  facdiv  10920  facwordi  10922  faclbnd  10923  fundm2domnop0  11027  swrdswrdlem  11195  swrdswrd  11196  ccatopth2  11208  wrd2ind  11214  pfxccatin12lem2a  11218  swrdccatin2  11220  pfxccatin12lem2  11222  pfxccatin12lem3  11223  swrdccat  11226  swrdccat3blem  11230  reuccatpfxs1lem  11237  cau3lem  11540  mulcn2  11738  climcau  11773  climcaucn  11777  modfsummod  11884  p1modz1  12220  dvdsdivcl  12276  ltoddhalfle  12319  halfleoddlt  12320  ndvdssub  12356  dfgcd2  12450  coprmdvds1  12528  coprmdvds  12529  coprmdvds2  12530  divgcdcoprm0  12538  cncongr1  12540  cncongr2  12541  prmfac1  12589  pcqcl  12744  dvdsprmpweqle  12775  oddprmdvds  12792  prmpwdvds  12793  infpnlem1  12797  lidrididd  13329  mulgaddcom  13597  mulginvcom  13598  imasabl  13787  lmodfopnelem1  14201  lss1d  14260  rnglidlmcl  14357  znrrg  14537  uniopn  14588  tgcnp  14796  iscnp4  14805  lmtopcnp  14837  txlm  14866  metss  15081  metcnp3  15098  logbgcd1irr  15554  gausslemma2dlem1a  15650  gausslemma2dlem2  15654  gausslemma2dlem3  15655  lgsquad2lem2  15674  2lgslem1a1  15678  2sqlem6  15712  upgredgpr  15853  bj-rspgt  15922