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  2763  vtoclgft  2787  reu6  2926  sbciegft  2993  reuss2  3415  reupick  3419  reusv3  4460  ssrel  4714  ssrel2  4716  ssrelrel  4726  funssres  5258  funcnvuni  5285  fv3  5538  fvmptt  5607  funfvima2  5749  isoini  5818  isopolem  5822  f1ocnv2d  6074  f1o2ndf1  6228  nnmordi  6516  nnmord  6517  xpdom2  6830  findcard2  6888  findcard2s  6889  findcard2d  6890  findcard2sd  6891  xpfi  6928  ordiso2  7033  updjud  7080  genpcdl  7517  genpcuu  7518  distrlem5prl  7584  distrlem5pru  7585  lemul12a  8817  divgt0  8827  divge0  8828  lbreu  8900  bndndx  9173  elnnz  9261  nzadd  9303  fzind  9366  fnn0ind  9367  eqreznegel  9612  lbzbi  9614  irradd  9644  irrmul  9645  ledivge1le  9724  iccid  9923  uzsubsubfz  10044  fzrevral  10102  elfz0fzfz0  10123  fz0fzelfz0  10124  elfzmlbp  10129  elfzodifsumelfzo  10198  ssfzo12bi  10222  elfzonelfzo  10227  flqeqceilz  10315  le2sq2  10592  facdiv  10713  facwordi  10715  faclbnd  10716  cau3lem  11118  mulcn2  11315  climcau  11350  climcaucn  11354  modfsummod  11461  p1modz1  11796  dvdsdivcl  11850  ltoddhalfle  11892  halfleoddlt  11893  ndvdssub  11929  dfgcd2  12009  coprmdvds1  12085  coprmdvds  12086  coprmdvds2  12087  divgcdcoprm0  12095  cncongr1  12097  cncongr2  12098  prmfac1  12146  pcqcl  12300  dvdsprmpweqle  12330  oddprmdvds  12346  prmpwdvds  12347  infpnlem1  12351  lidrididd  12795  mulgaddcom  13000  mulginvcom  13001  uniopn  13432  tgcnp  13640  iscnp4  13649  lmtopcnp  13681  txlm  13710  metss  13925  metcnp3  13942  logbgcd1irr  14316  2sqlem6  14387  bj-rspgt  14458