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  627  impidc  863  pm2.61dc  870  3com23  1233  expcomd  1484  spimth  1781  sbiedh  1833  eqrdav  2228  necon4bbiddc  2474  ralrimdva  2610  ralrimdvva  2615  ceqsalt  2826  vtoclgft  2851  reu6  2992  sbciegft  3059  reuss2  3484  reupick  3488  reusv3  4551  ssrel  4807  ssrel2  4809  ssrelrel  4819  ssrelrn  4914  funssres  5360  funcnvuni  5390  fv3  5652  fvmptt  5728  funfvima2  5876  isoini  5948  isopolem  5952  f1ocnv2d  6216  f1o2ndf1  6380  nnmordi  6670  nnmord  6671  xpdom2  6998  findcard2  7059  findcard2s  7060  findcard2d  7061  findcard2sd  7062  xpfi  7105  ordiso2  7213  updjud  7260  genpcdl  7717  genpcuu  7718  distrlem5prl  7784  distrlem5pru  7785  lemul12a  9020  divgt0  9030  divge0  9031  lbreu  9103  bndndx  9379  elnnz  9467  nzadd  9510  fzind  9573  fnn0ind  9574  eqreznegel  9821  lbzbi  9823  irradd  9853  irrmul  9854  ledivge1le  9934  iccid  10133  uzsubsubfz  10255  fzrevral  10313  elfz0fzfz0  10334  fz0fzelfz0  10335  elfzmlbp  10340  elincfzoext  10411  elfzodifsumelfzo  10419  ssfzo12bi  10443  elfzonelfzo  10448  flqeqceilz  10552  le2sq2  10849  facdiv  10972  facwordi  10974  faclbnd  10975  fundm2domnop0  11080  swrdswrdlem  11252  swrdswrd  11253  ccatopth2  11265  wrd2ind  11271  pfxccatin12lem2a  11275  swrdccatin2  11277  pfxccatin12lem2  11279  pfxccatin12lem3  11280  swrdccat  11283  swrdccat3blem  11287  reuccatpfxs1lem  11294  cau3lem  11641  mulcn2  11839  climcau  11874  climcaucn  11878  modfsummod  11985  p1modz1  12321  dvdsdivcl  12377  ltoddhalfle  12420  halfleoddlt  12421  ndvdssub  12457  dfgcd2  12551  coprmdvds1  12629  coprmdvds  12630  coprmdvds2  12631  divgcdcoprm0  12639  cncongr1  12641  cncongr2  12642  prmfac1  12690  pcqcl  12845  dvdsprmpweqle  12876  oddprmdvds  12893  prmpwdvds  12894  infpnlem1  12898  lidrididd  13431  mulgaddcom  13699  mulginvcom  13700  imasabl  13889  lmodfopnelem1  14304  lss1d  14363  rnglidlmcl  14460  znrrg  14640  uniopn  14691  tgcnp  14899  iscnp4  14908  lmtopcnp  14940  txlm  14969  metss  15184  metcnp3  15201  logbgcd1irr  15657  gausslemma2dlem1a  15753  gausslemma2dlem2  15757  gausslemma2dlem3  15758  lgsquad2lem2  15777  2lgslem1a1  15781  2sqlem6  15815  umgrnloop  15932  upgredgpr  15963  usgrausgrben  15986  usgredg2vlem2  16037  ushgredgedg  16040  ushgredgedgloop  16042  wlk1walkdom  16105  uspgr2wlkeqi  16113  clwwlk1loop  16142  clwwlkccatlem  16143  umgrclwwlkge2  16145  bj-rspgt  16233