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  560  con2d  629  impidc  865  pm2.61dc  872  3com23  1235  expcomd  1486  spimth  1783  sbiedh  1835  eqrdav  2230  necon4bbiddc  2476  ralrimdva  2612  ralrimdvva  2617  ceqsalt  2829  vtoclgft  2854  reu6  2995  sbciegft  3062  reuss2  3487  reupick  3491  reusv3  4557  ssrel  4814  ssrel2  4816  ssrelrel  4826  ssrelrn  4922  funssres  5369  funcnvuni  5399  f1ssf1  5615  fv3  5662  fvmptt  5738  funfvima2  5887  isoini  5959  isopolem  5963  f1ocnv2d  6227  f1o2ndf1  6393  nnmordi  6684  nnmord  6685  xpdom2  7015  findcard2  7078  findcard2s  7079  findcard2d  7080  findcard2sd  7081  xpfi  7124  ordiso2  7234  updjud  7281  genpcdl  7739  genpcuu  7740  distrlem5prl  7806  distrlem5pru  7807  lemul12a  9042  divgt0  9052  divge0  9053  lbreu  9125  bndndx  9401  elnnz  9489  nzadd  9532  fzind  9595  fnn0ind  9596  eqreznegel  9848  lbzbi  9850  irradd  9880  irrmul  9881  ledivge1le  9961  iccid  10160  uzsubsubfz  10282  fzrevral  10340  elfz0fzfz0  10361  fz0fzelfz0  10362  elfzmlbp  10367  elincfzoext  10439  elfzodifsumelfzo  10447  ssfzo12bi  10471  elfzonelfzo  10476  flqeqceilz  10581  le2sq2  10878  facdiv  11001  facwordi  11003  faclbnd  11004  fundm2domnop0  11113  swrdswrdlem  11289  swrdswrd  11290  ccatopth2  11302  wrd2ind  11308  pfxccatin12lem2a  11312  swrdccatin2  11314  pfxccatin12lem2  11316  pfxccatin12lem3  11317  swrdccat  11320  swrdccat3blem  11324  reuccatpfxs1lem  11331  cau3lem  11692  mulcn2  11890  climcau  11925  climcaucn  11929  modfsummod  12037  p1modz1  12373  dvdsdivcl  12429  ltoddhalfle  12472  halfleoddlt  12473  ndvdssub  12509  dfgcd2  12603  coprmdvds1  12681  coprmdvds  12682  coprmdvds2  12683  divgcdcoprm0  12691  cncongr1  12693  cncongr2  12694  prmfac1  12742  pcqcl  12897  dvdsprmpweqle  12928  oddprmdvds  12945  prmpwdvds  12946  infpnlem1  12950  lidrididd  13483  mulgaddcom  13751  mulginvcom  13752  imasabl  13941  lmodfopnelem1  14357  lss1d  14416  rnglidlmcl  14513  znrrg  14693  uniopn  14744  tgcnp  14952  iscnp4  14961  lmtopcnp  14993  txlm  15022  metss  15237  metcnp3  15254  logbgcd1irr  15710  gausslemma2dlem1a  15806  gausslemma2dlem2  15810  gausslemma2dlem3  15811  lgsquad2lem2  15830  2lgslem1a1  15834  2sqlem6  15868  umgrnloop  15986  upgredgpr  16019  usgrausgrben  16042  usgredg2vlem2  16093  ushgredgedg  16096  ushgredgedgloop  16098  wlk1walkdom  16229  uspgr2wlkeqi  16237  clwwlk1loop  16269  clwwlkccatlem  16270  umgrclwwlkge2  16272  clwwlknonex2lem2  16308  clwwlknonex2  16309  bj-rspgt  16433  gfsumval  16732