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  558  con2d  627  impidc  863  pm2.61dc  870  3com23  1233  expcomd  1484  spimth  1781  sbiedh  1833  eqrdav  2228  necon4bbiddc  2474  ralrimdva  2610  ralrimdvva  2615  ceqsalt  2827  vtoclgft  2852  reu6  2993  sbciegft  3060  reuss2  3485  reupick  3489  reusv3  4555  ssrel  4812  ssrel2  4814  ssrelrel  4824  ssrelrn  4920  funssres  5366  funcnvuni  5396  fv3  5658  fvmptt  5734  funfvima2  5882  isoini  5954  isopolem  5958  f1ocnv2d  6222  f1o2ndf1  6388  nnmordi  6679  nnmord  6680  xpdom2  7010  findcard2  7071  findcard2s  7072  findcard2d  7073  findcard2sd  7074  xpfi  7117  ordiso2  7225  updjud  7272  genpcdl  7729  genpcuu  7730  distrlem5prl  7796  distrlem5pru  7797  lemul12a  9032  divgt0  9042  divge0  9043  lbreu  9115  bndndx  9391  elnnz  9479  nzadd  9522  fzind  9585  fnn0ind  9586  eqreznegel  9838  lbzbi  9840  irradd  9870  irrmul  9871  ledivge1le  9951  iccid  10150  uzsubsubfz  10272  fzrevral  10330  elfz0fzfz0  10351  fz0fzelfz0  10352  elfzmlbp  10357  elincfzoext  10428  elfzodifsumelfzo  10436  ssfzo12bi  10460  elfzonelfzo  10465  flqeqceilz  10570  le2sq2  10867  facdiv  10990  facwordi  10992  faclbnd  10993  fundm2domnop0  11099  swrdswrdlem  11275  swrdswrd  11276  ccatopth2  11288  wrd2ind  11294  pfxccatin12lem2a  11298  swrdccatin2  11300  pfxccatin12lem2  11302  pfxccatin12lem3  11303  swrdccat  11306  swrdccat3blem  11310  reuccatpfxs1lem  11317  cau3lem  11665  mulcn2  11863  climcau  11898  climcaucn  11902  modfsummod  12009  p1modz1  12345  dvdsdivcl  12401  ltoddhalfle  12444  halfleoddlt  12445  ndvdssub  12481  dfgcd2  12575  coprmdvds1  12653  coprmdvds  12654  coprmdvds2  12655  divgcdcoprm0  12663  cncongr1  12665  cncongr2  12666  prmfac1  12714  pcqcl  12869  dvdsprmpweqle  12900  oddprmdvds  12917  prmpwdvds  12918  infpnlem1  12922  lidrididd  13455  mulgaddcom  13723  mulginvcom  13724  imasabl  13913  lmodfopnelem1  14328  lss1d  14387  rnglidlmcl  14484  znrrg  14664  uniopn  14715  tgcnp  14923  iscnp4  14932  lmtopcnp  14964  txlm  14993  metss  15208  metcnp3  15225  logbgcd1irr  15681  gausslemma2dlem1a  15777  gausslemma2dlem2  15781  gausslemma2dlem3  15782  lgsquad2lem2  15801  2lgslem1a1  15805  2sqlem6  15839  umgrnloop  15957  upgredgpr  15988  usgrausgrben  16011  usgredg2vlem2  16062  ushgredgedg  16065  ushgredgedgloop  16067  wlk1walkdom  16156  uspgr2wlkeqi  16164  clwwlk1loop  16194  clwwlkccatlem  16195  umgrclwwlkge2  16197  clwwlknonex2lem2  16233  clwwlknonex2  16234  bj-rspgt  16318