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  7376  updjud  7423  genpcdl  7887  genpcuu  7888  distrlem5prl  7954  distrlem5pru  7955  lemul12a  9195  divgt0  9205  divge0  9206  lbreu  9278  bndndx  9567  elnnz  9659  nzadd  9702  fzind  9766  fnn0ind  9767  eqreznegel  10024  lbzbi  10026  irradd  10056  irrmul  10058  ledivge1le  10138  iccid  10338  uzsubsubfz  10463  fzrevral  10523  elfz0fzfz0  10544  fz0fzelfz0  10545  elfzmlbp  10550  elincfzoext  10622  elfzodifsumelfzo  10630  ssfzo12bi  10654  elfzonelfzo  10659  flqeqceilz  10770  le2sq2  11067  facdiv  11192  facwordi  11194  faclbnd  11195  fundm2domnop0  11316  swrdswrdlem  11492  swrdswrd  11493  ccatopth2  11505  wrd2ind  11511  pfxccatin12lem2a  11515  swrdccatin2  11517  pfxccatin12lem2  11519  pfxccatin12lem3  11520  swrdccat  11523  swrdccat3blem  11527  reuccatpfxs1lem  11534  cau3lem  11897  mulcn2  12097  climcau  12132  climcaucn  12136  modfsummod  12244  p1modz1  12580  dvdsdivcl  12636  ltoddhalfle  12679  halfleoddlt  12680  ndvdssub  12716  dfgcd2  12810  coprmdvds1  12888  coprmdvds  12889  coprmdvds2  12890  divgcdcoprm0  12898  cncongr1  12900  cncongr2  12901  prmfac1  12950  pcqcl  13108  dvdsprmpweqle  13139  oddprmdvds  13156  prmpwdvds  13157  infpnlem1  13161  lidrididd  13755  mulgaddcom  14002  mulginvcom  14003  imasabl  14224  gsumvalfi  14236  lmodfopnelem1  14745  lss1d  14804  rnglidlmcl  14901  znrrg  15079  uniopn  15193  tgcnp  15401  iscnp4  15410  lmtopcnp  15442  txlm  15471  metss  15686  metcnp3  15703  logbgcd1irr  16164  gausslemma2dlem1a  16343  gausslemma2dlem2  16347  gausslemma2dlem3  16348  lgsquad2lem2  16367  2lgslem1a1  16371  2sqlem6  16405  umgrnloop  16523  upgredgpr  16556  usgrausgrben  16579  usgredg2vlem2  16630  ushgredgedg  16633  ushgredgedgloop  16635  wlk1walkdom  16766  uspgr2wlkeqi  16774  clwwlk1loop  16806  clwwlkccatlem  16807  umgrclwwlkge2  16809  clwwlknonex2lem2  16845  clwwlknonex2  16846  lealltlt2  16918  bj-rspgt  16980