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  6794  nnmord  6795  xpdom2  7135  findcard2  7199  findcard2s  7200  findcard2d  7201  findcard2sd  7202  xpfi  7245  ordiso2  7381  updjud  7428  genpcdl  7892  genpcuu  7893  distrlem5prl  7959  distrlem5pru  7960  lemul12a  9200  divgt0  9210  divge0  9211  lbreu  9283  bndndx  9573  elnnz  9663  nzadd  9706  fzind  9771  fnn0ind  9772  eqreznegel  10029  lbzbi  10031  irradd  10061  irrmul  10063  ledivge1le  10143  iccid  10343  uzsubsubfz  10468  fzrevral  10528  elfz0fzfz0  10549  fz0fzelfz0  10550  elfzmlbp  10555  elincfzoext  10627  elfzodifsumelfzo  10635  ssfzo12bi  10659  elfzonelfzo  10664  flqeqceilz  10775  le2sq2  11072  facdiv  11197  facwordi  11199  faclbnd  11200  fundm2domnop0  11321  swrdswrdlem  11497  swrdswrd  11498  ccatopth2  11510  wrd2ind  11516  pfxccatin12lem2a  11520  swrdccatin2  11522  pfxccatin12lem2  11524  pfxccatin12lem3  11525  swrdccat  11528  swrdccat3blem  11532  reuccatpfxs1lem  11539  cau3lem  11902  mulcn2  12102  climcau  12137  climcaucn  12141  modfsummod  12249  p1modz1  12585  dvdsdivcl  12641  ltoddhalfle  12684  halfleoddlt  12685  ndvdssub  12721  dfgcd2  12815  coprmdvds1  12893  coprmdvds  12894  coprmdvds2  12895  divgcdcoprm0  12903  cncongr1  12905  cncongr2  12906  prmfac1  12955  pcqcl  13113  dvdsprmpweqle  13144  oddprmdvds  13161  prmpwdvds  13162  infpnlem1  13166  lidrididd  13760  mulgaddcom  14007  mulginvcom  14008  imasabl  14229  gsumvalfi  14241  lmodfopnelem1  14769  lss1d  14828  rnglidlmcl  14925  znrrg  15103  uniopn  15244  tgcnp  15452  iscnp4  15461  lmtopcnp  15493  txlm  15522  metss  15737  metcnp3  15754  logbgcd1irr  16220  gausslemma2dlem1a  16399  gausslemma2dlem2  16403  gausslemma2dlem3  16404  lgsquad2lem2  16423  2lgslem1a1  16427  2sqlem6  16461  umgrnloop  16579  upgredgpr  16612  usgrausgrben  16635  usgredg2vlem2  16686  ushgredgedg  16689  ushgredgedgloop  16691  wlk1walkdom  16822  uspgr2wlkeqi  16830  clwwlk1loop  16862  clwwlkccatlem  16863  umgrclwwlkge2  16865  clwwlknonex2lem2  16901  clwwlknonex2  16902  lealltlt2  16974  bj-rspgt  17036