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  99  impcomd  253  impancom  258  a2and  553  con2d  619  impidc  853  pm2.61dc  860  3com23  1204  expcomd  1434  spimth  1728  sbiedh  1780  eqrdav  2169  necon4bbiddc  2414  ralrimdva  2550  ralrimdvva  2555  ceqsalt  2756  vtoclgft  2780  reu6  2919  sbciegft  2985  reuss2  3407  reupick  3411  reusv3  4445  ssrel  4699  ssrel2  4701  ssrelrel  4711  funssres  5240  funcnvuni  5267  fv3  5519  fvmptt  5587  funfvima2  5728  isoini  5797  isopolem  5801  f1ocnv2d  6053  f1o2ndf1  6207  nnmordi  6495  nnmord  6496  xpdom2  6809  findcard2  6867  findcard2s  6868  findcard2d  6869  findcard2sd  6870  xpfi  6907  ordiso2  7012  updjud  7059  genpcdl  7481  genpcuu  7482  distrlem5prl  7548  distrlem5pru  7549  lemul12a  8778  divgt0  8788  divge0  8789  lbreu  8861  bndndx  9134  elnnz  9222  nzadd  9264  fzind  9327  fnn0ind  9328  eqreznegel  9573  lbzbi  9575  irradd  9605  irrmul  9606  ledivge1le  9683  iccid  9882  uzsubsubfz  10003  fzrevral  10061  elfz0fzfz0  10082  fz0fzelfz0  10083  elfzmlbp  10088  elfzodifsumelfzo  10157  ssfzo12bi  10181  elfzonelfzo  10186  flqeqceilz  10274  le2sq2  10551  facdiv  10672  facwordi  10674  faclbnd  10675  cau3lem  11078  mulcn2  11275  climcau  11310  climcaucn  11314  modfsummod  11421  p1modz1  11756  dvdsdivcl  11810  ltoddhalfle  11852  halfleoddlt  11853  ndvdssub  11889  dfgcd2  11969  coprmdvds1  12045  coprmdvds  12046  coprmdvds2  12047  divgcdcoprm0  12055  cncongr1  12057  cncongr2  12058  prmfac1  12106  pcqcl  12260  dvdsprmpweqle  12290  oddprmdvds  12306  prmpwdvds  12307  infpnlem1  12311  lidrididd  12636  uniopn  12793  tgcnp  13003  iscnp4  13012  lmtopcnp  13044  txlm  13073  metss  13288  metcnp3  13305  logbgcd1irr  13679  2sqlem6  13750  bj-rspgt  13821