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  866  pm2.61dc  873  3com23  1236  expcomd  1487  spimth  1784  sbiedh  1836  eqrdav  2231  necon4bbiddc  2486  ralrimdva  2622  ralrimdvva  2627  ceqsalt  2840  vtoclgft  2865  reu6  3006  sbciegft  3073  reuss2  3501  reupick  3505  reusv3  4581  ssrel  4838  ssrel2  4840  ssrelrel  4850  ssrelrn  4947  funssres  5395  funcnvuni  5425  f1ssf1  5646  fv3  5693  fvmptt  5769  funfvima2  5919  isoini  5991  isopolem  5995  f1ocnv2d  6259  f1o2ndf1  6424  suppfnss  6457  suppssdc  6460  nnmordi  6749  nnmord  6750  xpdom2  7082  findcard2  7146  findcard2s  7147  findcard2d  7148  findcard2sd  7149  xpfi  7192  ordiso2  7326  updjud  7373  genpcdl  7834  genpcuu  7835  distrlem5prl  7901  distrlem5pru  7902  lemul12a  9136  divgt0  9146  divge0  9147  lbreu  9219  bndndx  9495  elnnz  9587  nzadd  9630  fzind  9693  fnn0ind  9694  eqreznegel  9946  lbzbi  9948  irradd  9978  irrmul  9979  ledivge1le  10059  iccid  10258  uzsubsubfz  10381  fzrevral  10439  elfz0fzfz0  10460  fz0fzelfz0  10461  elfzmlbp  10466  elincfzoext  10538  elfzodifsumelfzo  10546  ssfzo12bi  10570  elfzonelfzo  10575  flqeqceilz  10680  le2sq2  10977  facdiv  11100  facwordi  11102  faclbnd  11103  fundm2domnop0  11220  swrdswrdlem  11396  swrdswrd  11397  ccatopth2  11409  wrd2ind  11415  pfxccatin12lem2a  11419  swrdccatin2  11421  pfxccatin12lem2  11423  pfxccatin12lem3  11424  swrdccat  11427  swrdccat3blem  11431  reuccatpfxs1lem  11438  cau3lem  11799  mulcn2  11997  climcau  12032  climcaucn  12036  modfsummod  12144  p1modz1  12480  dvdsdivcl  12536  ltoddhalfle  12579  halfleoddlt  12580  ndvdssub  12616  dfgcd2  12710  coprmdvds1  12788  coprmdvds  12789  coprmdvds2  12790  divgcdcoprm0  12798  cncongr1  12800  cncongr2  12801  prmfac1  12849  pcqcl  13004  dvdsprmpweqle  13035  oddprmdvds  13052  prmpwdvds  13053  infpnlem1  13057  lidrididd  13595  mulgaddcom  13863  mulginvcom  13864  imasabl  14053  lmodfopnelem1  14472  lss1d  14531  rnglidlmcl  14628  znrrg  14808  uniopn  14866  tgcnp  15074  iscnp4  15083  lmtopcnp  15115  txlm  15144  metss  15359  metcnp3  15376  logbgcd1irr  15832  gausslemma2dlem1a  15931  gausslemma2dlem2  15935  gausslemma2dlem3  15936  lgsquad2lem2  15955  2lgslem1a1  15959  2sqlem6  15993  umgrnloop  16111  upgredgpr  16144  usgrausgrben  16167  usgredg2vlem2  16218  ushgredgedg  16221  ushgredgedgloop  16223  wlk1walkdom  16354  uspgr2wlkeqi  16362  clwwlk1loop  16394  clwwlkccatlem  16395  umgrclwwlkge2  16397  clwwlknonex2lem2  16433  clwwlknonex2  16434  bj-rspgt  16558  gfsumval  16862