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  625  impidc  860  pm2.61dc  867  3com23  1212  expcomd  1461  spimth  1758  sbiedh  1810  eqrdav  2204  necon4bbiddc  2450  ralrimdva  2586  ralrimdvva  2591  ceqsalt  2798  vtoclgft  2823  reu6  2962  sbciegft  3029  reuss2  3453  reupick  3457  reusv3  4507  ssrel  4763  ssrel2  4765  ssrelrel  4775  funssres  5313  funcnvuni  5343  fv3  5599  fvmptt  5671  funfvima2  5817  isoini  5887  isopolem  5891  f1ocnv2d  6150  f1o2ndf1  6314  nnmordi  6602  nnmord  6603  xpdom2  6926  findcard2  6986  findcard2s  6987  findcard2d  6988  findcard2sd  6989  xpfi  7029  ordiso2  7137  updjud  7184  genpcdl  7632  genpcuu  7633  distrlem5prl  7699  distrlem5pru  7700  lemul12a  8935  divgt0  8945  divge0  8946  lbreu  9018  bndndx  9294  elnnz  9382  nzadd  9425  fzind  9488  fnn0ind  9489  eqreznegel  9735  lbzbi  9737  irradd  9767  irrmul  9768  ledivge1le  9848  iccid  10047  uzsubsubfz  10169  fzrevral  10227  elfz0fzfz0  10248  fz0fzelfz0  10249  elfzmlbp  10254  elincfzoext  10322  elfzodifsumelfzo  10330  ssfzo12bi  10354  elfzonelfzo  10359  flqeqceilz  10463  le2sq2  10760  facdiv  10883  facwordi  10885  faclbnd  10886  fundm2domnop0  10990  cau3lem  11425  mulcn2  11623  climcau  11658  climcaucn  11662  modfsummod  11769  p1modz1  12105  dvdsdivcl  12161  ltoddhalfle  12204  halfleoddlt  12205  ndvdssub  12241  dfgcd2  12335  coprmdvds1  12413  coprmdvds  12414  coprmdvds2  12415  divgcdcoprm0  12423  cncongr1  12425  cncongr2  12426  prmfac1  12474  pcqcl  12629  dvdsprmpweqle  12660  oddprmdvds  12677  prmpwdvds  12678  infpnlem1  12682  lidrididd  13214  mulgaddcom  13482  mulginvcom  13483  imasabl  13672  lmodfopnelem1  14086  lss1d  14145  rnglidlmcl  14242  znrrg  14422  uniopn  14473  tgcnp  14681  iscnp4  14690  lmtopcnp  14722  txlm  14751  metss  14966  metcnp3  14983  logbgcd1irr  15439  gausslemma2dlem1a  15535  gausslemma2dlem2  15539  gausslemma2dlem3  15540  lgsquad2lem2  15559  2lgslem1a1  15563  2sqlem6  15597  bj-rspgt  15722