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

Syntax hints:   -> wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is referenced by:  com3r  79  com13  80  pm2.04  82  pm2.86d  100  impcomd  255  impancom  260  a2and  560  con2d  629  impidc  865  pm2.61dc  872  3com23  1235  expcomd  1486  spimth  1783  sbiedh  1835  eqrdav  2230  necon4bbiddc  2476  ralrimdva  2612  ralrimdvva  2617  ceqsalt  2829  vtoclgft  2854  reu6  2995  sbciegft  3062  reuss2  3487  reupick  3491  reusv3  4557  ssrel  4814  ssrel2  4816  ssrelrel  4826  ssrelrn  4922  funssres  5369  funcnvuni  5399  f1ssf1  5615  fv3  5662  fvmptt  5738  funfvima2  5886  isoini  5958  isopolem  5962  f1ocnv2d  6226  f1o2ndf1  6392  nnmordi  6683  nnmord  6684  xpdom2  7014  findcard2  7077  findcard2s  7078  findcard2d  7079  findcard2sd  7080  xpfi  7123  ordiso2  7233  updjud  7280  genpcdl  7738  genpcuu  7739  distrlem5prl  7805  distrlem5pru  7806  lemul12a  9041  divgt0  9051  divge0  9052  lbreu  9124  bndndx  9400  elnnz  9488  nzadd  9531  fzind  9594  fnn0ind  9595  eqreznegel  9847  lbzbi  9849  irradd  9879  irrmul  9880  ledivge1le  9960  iccid  10159  uzsubsubfz  10281  fzrevral  10339  elfz0fzfz0  10360  fz0fzelfz0  10361  elfzmlbp  10366  elincfzoext  10437  elfzodifsumelfzo  10445  ssfzo12bi  10469  elfzonelfzo  10474  flqeqceilz  10579  le2sq2  10876  facdiv  10999  facwordi  11001  faclbnd  11002  fundm2domnop0  11108  swrdswrdlem  11284  swrdswrd  11285  ccatopth2  11297  wrd2ind  11303  pfxccatin12lem2a  11307  swrdccatin2  11309  pfxccatin12lem2  11311  pfxccatin12lem3  11312  swrdccat  11315  swrdccat3blem  11319  reuccatpfxs1lem  11326  cau3lem  11674  mulcn2  11872  climcau  11907  climcaucn  11911  modfsummod  12018  p1modz1  12354  dvdsdivcl  12410  ltoddhalfle  12453  halfleoddlt  12454  ndvdssub  12490  dfgcd2  12584  coprmdvds1  12662  coprmdvds  12663  coprmdvds2  12664  divgcdcoprm0  12672  cncongr1  12674  cncongr2  12675  prmfac1  12723  pcqcl  12878  dvdsprmpweqle  12909  oddprmdvds  12926  prmpwdvds  12927  infpnlem1  12931  lidrididd  13464  mulgaddcom  13732  mulginvcom  13733  imasabl  13922  lmodfopnelem1  14337  lss1d  14396  rnglidlmcl  14493  znrrg  14673  uniopn  14724  tgcnp  14932  iscnp4  14941  lmtopcnp  14973  txlm  15002  metss  15217  metcnp3  15234  logbgcd1irr  15690  gausslemma2dlem1a  15786  gausslemma2dlem2  15790  gausslemma2dlem3  15791  lgsquad2lem2  15810  2lgslem1a1  15814  2sqlem6  15848  umgrnloop  15966  upgredgpr  15999  usgrausgrben  16022  usgredg2vlem2  16073  ushgredgedg  16076  ushgredgedgloop  16078  wlk1walkdom  16209  uspgr2wlkeqi  16217  clwwlk1loop  16249  clwwlkccatlem  16250  umgrclwwlkge2  16252  clwwlknonex2lem2  16288  clwwlknonex2  16289  bj-rspgt  16382  gfsumval  16680