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  4608  ssrel  4865  ssrel2  4867  ssrelrel  4877  ssrelrn  4974  funssres  5423  funcnvuni  5453  f1ssf1  5674  fv3  5721  fvmptt  5800  funfvima2  5954  isoini  6027  isopolem  6031  f1ocnv2d  6297  f1o3d  6301  f1o2ndf1  6468  suppfnss  6501  suppssdc  6504  nnmordi  6793  nnmord  6794  xpdom2  7133  findcard2  7197  findcard2s  7198  findcard2d  7199  findcard2sd  7200  xpfi  7243  ordiso2  7381  updjud  7428  genpcdl  7892  genpcuu  7893  distrlem5prl  7959  distrlem5pru  7960  lemul12a  9200  divgt0  9210  divge0  9211  lbreu  9283  bndndx  9573  elnnz  9665  nzadd  9708  fzind  9772  fnn0ind  9773  eqreznegel  10030  lbzbi  10032  irradd  10062  irrmul  10064  ledivge1le  10144  iccid  10344  uzsubsubfz  10469  fzrevral  10529  elfz0fzfz0  10550  fz0fzelfz0  10551  elfzmlbp  10556  elincfzoext  10628  elfzodifsumelfzo  10636  ssfzo12bi  10660  elfzonelfzo  10665  flqeqceilz  10776  le2sq2  11073  facdiv  11198  facwordi  11200  faclbnd  11201  fundm2domnop0  11322  swrdswrdlem  11498  swrdswrd  11499  ccatopth2  11511  wrd2ind  11517  pfxccatin12lem2a  11521  swrdccatin2  11523  pfxccatin12lem2  11525  pfxccatin12lem3  11526  swrdccat  11529  swrdccat3blem  11533  reuccatpfxs1lem  11540  cau3lem  11903  mulcn2  12103  climcau  12138  climcaucn  12142  modfsummod  12250  p1modz1  12586  dvdsdivcl  12642  ltoddhalfle  12685  halfleoddlt  12686  ndvdssub  12722  dfgcd2  12816  coprmdvds1  12894  coprmdvds  12895  coprmdvds2  12896  divgcdcoprm0  12904  cncongr1  12906  cncongr2  12907  prmfac1  12956  pcqcl  13114  dvdsprmpweqle  13145  oddprmdvds  13162  prmpwdvds  13163  infpnlem1  13167  lidrididd  13761  mulgaddcom  14008  mulginvcom  14009  imasabl  14230  gsumvalfi  14242  lmodfopnelem1  14770  lss1d  14829  rnglidlmcl  14926  znrrg  15104  uniopn  15227  tgcnp  15435  iscnp4  15444  lmtopcnp  15476  txlm  15505  metss  15720  metcnp3  15737  logbgcd1irr  16203  gausslemma2dlem1a  16382  gausslemma2dlem2  16386  gausslemma2dlem3  16387  lgsquad2lem2  16406  2lgslem1a1  16410  2sqlem6  16444  umgrnloop  16562  upgredgpr  16595  usgrausgrben  16618  usgredg2vlem2  16669  ushgredgedg  16672  ushgredgedgloop  16674  wlk1walkdom  16805  uspgr2wlkeqi  16813  clwwlk1loop  16845  clwwlkccatlem  16846  umgrclwwlkge2  16848  clwwlknonex2lem2  16884  clwwlknonex2  16885  lealltlt2  16957  bj-rspgt  17019