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  9192  divgt0  9202  divge0  9203  lbreu  9275  bndndx  9562  elnnz  9654  nzadd  9697  fzind  9761  fnn0ind  9762  eqreznegel  10014  lbzbi  10016  irradd  10046  irrmul  10047  ledivge1le  10127  iccid  10327  uzsubsubfz  10452  fzrevral  10512  elfz0fzfz0  10533  fz0fzelfz0  10534  elfzmlbp  10539  elincfzoext  10611  elfzodifsumelfzo  10619  ssfzo12bi  10643  elfzonelfzo  10648  flqeqceilz  10755  le2sq2  11052  facdiv  11176  facwordi  11178  faclbnd  11179  fundm2domnop0  11300  swrdswrdlem  11476  swrdswrd  11477  ccatopth2  11489  wrd2ind  11495  pfxccatin12lem2a  11499  swrdccatin2  11501  pfxccatin12lem2  11503  pfxccatin12lem3  11504  swrdccat  11507  swrdccat3blem  11511  reuccatpfxs1lem  11518  cau3lem  11880  mulcn2  12078  climcau  12113  climcaucn  12117  modfsummod  12225  p1modz1  12561  dvdsdivcl  12617  ltoddhalfle  12660  halfleoddlt  12661  ndvdssub  12697  dfgcd2  12791  coprmdvds1  12869  coprmdvds  12870  coprmdvds2  12871  divgcdcoprm0  12879  cncongr1  12881  cncongr2  12882  prmfac1  12930  pcqcl  13085  dvdsprmpweqle  13116  oddprmdvds  13133  prmpwdvds  13134  infpnlem1  13138  lidrididd  13702  mulgaddcom  13949  mulginvcom  13950  imasabl  14140  gsumvalfi  14152  lmodfopnelem1  14661  lss1d  14720  rnglidlmcl  14817  znrrg  14995  uniopn  15102  tgcnp  15310  iscnp4  15319  lmtopcnp  15351  txlm  15380  metss  15595  metcnp3  15612  logbgcd1irr  16069  gausslemma2dlem1a  16177  gausslemma2dlem2  16181  gausslemma2dlem3  16182  lgsquad2lem2  16201  2lgslem1a1  16205  2sqlem6  16239  umgrnloop  16357  upgredgpr  16390  usgrausgrben  16413  usgredg2vlem2  16464  ushgredgedg  16467  ushgredgedgloop  16469  wlk1walkdom  16600  uspgr2wlkeqi  16608  clwwlk1loop  16640  clwwlkccatlem  16641  umgrclwwlkge2  16643  clwwlknonex2lem2  16679  clwwlknonex2  16680  lealltlt2  16752  bj-rspgt  16814