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-1 5  ax-2 6  ax-mp 7

This theorem is referenced by:  com3r  79  com13  80  pm2.04  82  pm2.86d  99  impcomd  253  impancom  258  a2and  530  con2d  596  impidc  826  pm2.61dc  833  3com23  1170  expcomd  1400  spimth  1696  sbiedh  1743  eqrdav  2114  necon4bbiddc  2356  ralrimdva  2486  ralrimdvva  2491  ceqsalt  2683  vtoclgft  2707  reu6  2842  sbciegft  2907  reuss2  3322  reupick  3326  reusv3  4341  ssrel  4587  ssrel2  4589  ssrelrel  4599  funssres  5123  funcnvuni  5150  fv3  5398  fvmptt  5466  funfvima2  5604  isoini  5673  isopolem  5677  f1ocnv2d  5928  f1o2ndf1  6079  nnmordi  6366  nnmord  6367  xpdom2  6678  findcard2  6736  findcard2s  6737  findcard2d  6738  findcard2sd  6739  xpfi  6771  ordiso2  6872  updjud  6919  genpcdl  7275  genpcuu  7276  distrlem5prl  7342  distrlem5pru  7343  lemul12a  8530  divgt0  8540  divge0  8541  lbreu  8613  bndndx  8880  elnnz  8968  nzadd  9010  fzind  9070  fnn0ind  9071  eqreznegel  9308  lbzbi  9310  irradd  9340  irrmul  9341  ledivge1le  9412  iccid  9601  uzsubsubfz  9720  fzrevral  9778  elfz0fzfz0  9796  fz0fzelfz0  9797  elfzmlbp  9802  elfzodifsumelfzo  9871  ssfzo12bi  9895  elfzonelfzo  9900  flqeqceilz  9984  le2sq2  10261  facdiv  10377  facwordi  10379  faclbnd  10380  cau3lem  10778  mulcn2  10973  climcau  11008  climcaucn  11012  modfsummod  11119  dvdsdivcl  11396  ltoddhalfle  11438  halfleoddlt  11439  ndvdssub  11475  dfgcd2  11548  coprmdvds1  11618  coprmdvds  11619  coprmdvds2  11620  divgcdcoprm0  11628  cncongr1  11630  cncongr2  11631  prmfac1  11676  uniopn  12011  tgcnp  12220  iscnp4  12229  lmtopcnp  12261  txlm  12290  metss  12483  metcnp3  12500  bj-rspgt  12685