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  624  impidc  858  pm2.61dc  865  3com23  1209  expcomd  1441  spimth  1735  sbiedh  1787  eqrdav  2176  necon4bbiddc  2421  ralrimdva  2557  ralrimdvva  2562  ceqsalt  2764  vtoclgft  2788  reu6  2927  sbciegft  2994  reuss2  3416  reupick  3420  reusv3  4461  ssrel  4715  ssrel2  4717  ssrelrel  4727  funssres  5259  funcnvuni  5286  fv3  5539  fvmptt  5608  funfvima2  5750  isoini  5819  isopolem  5823  f1ocnv2d  6075  f1o2ndf1  6229  nnmordi  6517  nnmord  6518  xpdom2  6831  findcard2  6889  findcard2s  6890  findcard2d  6891  findcard2sd  6892  xpfi  6929  ordiso2  7034  updjud  7081  genpcdl  7518  genpcuu  7519  distrlem5prl  7585  distrlem5pru  7586  lemul12a  8819  divgt0  8829  divge0  8830  lbreu  8902  bndndx  9175  elnnz  9263  nzadd  9305  fzind  9368  fnn0ind  9369  eqreznegel  9614  lbzbi  9616  irradd  9646  irrmul  9647  ledivge1le  9726  iccid  9925  uzsubsubfz  10047  fzrevral  10105  elfz0fzfz0  10126  fz0fzelfz0  10127  elfzmlbp  10132  elfzodifsumelfzo  10201  ssfzo12bi  10225  elfzonelfzo  10230  flqeqceilz  10318  le2sq2  10596  facdiv  10718  facwordi  10720  faclbnd  10721  cau3lem  11123  mulcn2  11320  climcau  11355  climcaucn  11359  modfsummod  11466  p1modz1  11801  dvdsdivcl  11856  ltoddhalfle  11898  halfleoddlt  11899  ndvdssub  11935  dfgcd2  12015  coprmdvds1  12091  coprmdvds  12092  coprmdvds2  12093  divgcdcoprm0  12101  cncongr1  12103  cncongr2  12104  prmfac1  12152  pcqcl  12306  dvdsprmpweqle  12336  oddprmdvds  12352  prmpwdvds  12353  infpnlem1  12357  lidrididd  12801  mulgaddcom  13007  mulginvcom  13008  lmodfopnelem1  13414  uniopn  13504  tgcnp  13712  iscnp4  13721  lmtopcnp  13753  txlm  13782  metss  13997  metcnp3  14014  logbgcd1irr  14388  2sqlem6  14470  bj-rspgt  14541