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  5650  fvmptt  5726  funfvima2  5872  isoini  5942  isopolem  5946  f1ocnv2d  6210  f1o2ndf1  6374  nnmordi  6662  nnmord  6663  xpdom2  6990  findcard2  7051  findcard2s  7052  findcard2d  7053  findcard2sd  7054  xpfi  7094  ordiso2  7202  updjud  7249  genpcdl  7706  genpcuu  7707  distrlem5prl  7773  distrlem5pru  7774  lemul12a  9009  divgt0  9019  divge0  9020  lbreu  9092  bndndx  9368  elnnz  9456  nzadd  9499  fzind  9562  fnn0ind  9563  eqreznegel  9809  lbzbi  9811  irradd  9841  irrmul  9842  ledivge1le  9922  iccid  10121  uzsubsubfz  10243  fzrevral  10301  elfz0fzfz0  10322  fz0fzelfz0  10323  elfzmlbp  10328  elincfzoext  10399  elfzodifsumelfzo  10407  ssfzo12bi  10431  elfzonelfzo  10436  flqeqceilz  10540  le2sq2  10837  facdiv  10960  facwordi  10962  faclbnd  10963  fundm2domnop0  11067  swrdswrdlem  11236  swrdswrd  11237  ccatopth2  11249  wrd2ind  11255  pfxccatin12lem2a  11259  swrdccatin2  11261  pfxccatin12lem2  11263  pfxccatin12lem3  11264  swrdccat  11267  swrdccat3blem  11271  reuccatpfxs1lem  11278  cau3lem  11625  mulcn2  11823  climcau  11858  climcaucn  11862  modfsummod  11969  p1modz1  12305  dvdsdivcl  12361  ltoddhalfle  12404  halfleoddlt  12405  ndvdssub  12441  dfgcd2  12535  coprmdvds1  12613  coprmdvds  12614  coprmdvds2  12615  divgcdcoprm0  12623  cncongr1  12625  cncongr2  12626  prmfac1  12674  pcqcl  12829  dvdsprmpweqle  12860  oddprmdvds  12877  prmpwdvds  12878  infpnlem1  12882  lidrididd  13415  mulgaddcom  13683  mulginvcom  13684  imasabl  13873  lmodfopnelem1  14288  lss1d  14347  rnglidlmcl  14444  znrrg  14624  uniopn  14675  tgcnp  14883  iscnp4  14892  lmtopcnp  14924  txlm  14953  metss  15168  metcnp3  15185  logbgcd1irr  15641  gausslemma2dlem1a  15737  gausslemma2dlem2  15741  gausslemma2dlem3  15742  lgsquad2lem2  15761  2lgslem1a1  15765  2sqlem6  15799  umgrnloop  15916  upgredgpr  15947  usgrausgrben  15970  usgredg2vlem2  16021  ushgredgedg  16024  ushgredgedgloop  16026  wlk1walkdom  16070  uspgr2wlkeqi  16078  bj-rspgt  16150