Theorem com23 77

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 39	. 2 |- ( ch -> ( ( ch -> th ) -> th ) )
3	1, 2	syl9 71	1 |- ( ph -> ( ch -> ( ps -> th ) ) )

Syntax hints:   -> wi 4

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

This theorem is referenced by:  com3r  78  com13  79  pm2.04  81  pm2.86d  98  impancom  256  con2d  586  impidc  788  pm2.61dc  795  3com23  1144  expcomd  1370  spimth  1663  sbiedh  1710  eqrdav  2080  necon4bbiddc  2319  ralrimdva  2441  ralrimdvva  2446  ceqsalt  2625  vtoclgft  2649  reu6  2781  sbciegft  2844  reuss2  3244  reupick  3248  reusv3  4210  ssrel  4446  ssrel2  4448  ssrelrel  4458  funssres  4962  funcnvuni  4988  fv3  5218  fvmptt  5283  funfvima2  5412  isoini  5477  isopolem  5481  f1ocnv2d  5724  f1o2ndf1  5869  nnmordi  6112  nnmord  6113  xpdom2  6328  findcard2  6373  findcard2s  6374  findcard2d  6375  findcard2sd  6376  ordiso2  6446  genpcdl  6709  genpcuu  6710  distrlem5prl  6776  distrlem5pru  6777  lemul12a  7940  divgt0  7950  divge0  7951  lbreu  8023  bndndx  8287  elnnz  8361  nzadd  8403  fzind  8462  fnn0ind  8463  eqreznegel  8699  lbzbi  8701  irradd  8731  irrmul  8732  ledivge1le  8803  iccid  8948  uzsubsubfz  9066  fzrevral  9122  elfz0fzfz0  9137  fz0fzelfz0  9138  elfzmlbp  9143  elfzodifsumelfzo  9210  ssfzo12bi  9234  elfzonelfzo  9239  flqeqceilz  9320  le2sq2  9551  facdiv  9665  facwordi  9667  faclbnd  9668  cau3lem  10000  mulcn2  10151  climcau  10184  climcaucn  10188  dvdsdivcl  10250  ltoddhalfle  10293  halfleoddlt  10294  ndvdssub  10330  dfgcd2  10403  coprmdvds1  10473  coprmdvds  10474  coprmdvds2  10475  divgcdcoprm0  10483  cncongr1  10485  cncongr2  10486  prmfac1  10531  bj-rspgt  10596