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 ) ) )

This proof depends on syntax axioms:   -> wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  com3r  79  com13  80  pm2.04  82  pm2.86d  100  impcomd  255  impancom  260  a2and  564  con2d  633  impidc  870  pm2.61dc  877  3com23  1240  expcomd  1491  spimth  1788  sbiedh  1840  eqrdav  2237  necon4bbiddc  2494  ralrimdva  2630  ralrimdvva  2635  ceqsalt  2848  vtoclgft  2873  reu6  3015  sbciegft  3082  reuss2  3513  reupick  3517  reusv3  4606  ssrel  4863  ssrel2  4865  ssrelrel  4875  ssrelrn  4972  funssres  5420  funcnvuni  5450  f1ssf1  5671  fv3  5718  fvmptt  5797  funfvima2  5951  isoini  6024  isopolem  6028  f1ocnv2d  6294  f1o3d  6298  f1o2ndf1  6464  suppfnss  6497  suppssdc  6500  nnmordi  6789  nnmord  6790  xpdom2  7129  findcard2  7193  findcard2s  7194  findcard2d  7195  findcard2sd  7196  xpfi  7239  ordiso2  7375  updjud  7422  genpcdl  7886  genpcuu  7887  distrlem5prl  7953  distrlem5pru  7954  lemul12a  9194  divgt0  9204  divge0  9205  lbreu  9277  bndndx  9566  elnnz  9658  nzadd  9701  fzind  9765  fnn0ind  9766  eqreznegel  10023  lbzbi  10025  irradd  10055  irrmul  10057  ledivge1le  10137  iccid  10337  uzsubsubfz  10462  fzrevral  10522  elfz0fzfz0  10543  fz0fzelfz0  10544  elfzmlbp  10549  elincfzoext  10621  elfzodifsumelfzo  10629  ssfzo12bi  10653  elfzonelfzo  10658  flqeqceilz  10768  le2sq2  11065  facdiv  11190  facwordi  11192  faclbnd  11193  fundm2domnop0  11314  swrdswrdlem  11490  swrdswrd  11491  ccatopth2  11503  wrd2ind  11509  pfxccatin12lem2a  11513  swrdccatin2  11515  pfxccatin12lem2  11517  pfxccatin12lem3  11518  swrdccat  11521  swrdccat3blem  11525  reuccatpfxs1lem  11532  cau3lem  11895  mulcn2  12094  climcau  12129  climcaucn  12133  modfsummod  12241  p1modz1  12577  dvdsdivcl  12633  ltoddhalfle  12676  halfleoddlt  12677  ndvdssub  12713  dfgcd2  12807  coprmdvds1  12885  coprmdvds  12886  coprmdvds2  12887  divgcdcoprm0  12895  cncongr1  12897  cncongr2  12898  prmfac1  12947  pcqcl  13105  dvdsprmpweqle  13136  oddprmdvds  13153  prmpwdvds  13154  infpnlem1  13158  lidrididd  13751  mulgaddcom  13998  mulginvcom  13999  imasabl  14189  gsumvalfi  14201  lmodfopnelem1  14710  lss1d  14769  rnglidlmcl  14866  znrrg  15044  uniopn  15151  tgcnp  15359  iscnp4  15368  lmtopcnp  15400  txlm  15429  metss  15644  metcnp3  15661  logbgcd1irr  16122  gausslemma2dlem1a  16275  gausslemma2dlem2  16279  gausslemma2dlem3  16280  lgsquad2lem2  16299  2lgslem1a1  16303  2sqlem6  16337  umgrnloop  16455  upgredgpr  16488  usgrausgrben  16511  usgredg2vlem2  16562  ushgredgedg  16565  ushgredgedgloop  16567  wlk1walkdom  16698  uspgr2wlkeqi  16706  clwwlk1loop  16738  clwwlkccatlem  16739  umgrclwwlkge2  16741  clwwlknonex2lem2  16777  clwwlknonex2  16778  lealltlt2  16850  bj-rspgt  16912