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  859  pm2.61dc  866  3com23  1211  expcomd  1452  spimth  1749  sbiedh  1801  eqrdav  2195  necon4bbiddc  2441  ralrimdva  2577  ralrimdvva  2582  ceqsalt  2789  vtoclgft  2814  reu6  2953  sbciegft  3020  reuss2  3444  reupick  3448  reusv3  4496  ssrel  4752  ssrel2  4754  ssrelrel  4764  funssres  5301  funcnvuni  5328  fv3  5584  fvmptt  5656  funfvima2  5798  isoini  5868  isopolem  5872  f1ocnv2d  6131  f1o2ndf1  6295  nnmordi  6583  nnmord  6584  xpdom2  6899  findcard2  6959  findcard2s  6960  findcard2d  6961  findcard2sd  6962  xpfi  7002  ordiso2  7110  updjud  7157  genpcdl  7605  genpcuu  7606  distrlem5prl  7672  distrlem5pru  7673  lemul12a  8908  divgt0  8918  divge0  8919  lbreu  8991  bndndx  9267  elnnz  9355  nzadd  9397  fzind  9460  fnn0ind  9461  eqreznegel  9707  lbzbi  9709  irradd  9739  irrmul  9740  ledivge1le  9820  iccid  10019  uzsubsubfz  10141  fzrevral  10199  elfz0fzfz0  10220  fz0fzelfz0  10221  elfzmlbp  10226  elfzodifsumelfzo  10296  ssfzo12bi  10320  elfzonelfzo  10325  flqeqceilz  10429  le2sq2  10726  facdiv  10849  facwordi  10851  faclbnd  10852  cau3lem  11298  mulcn2  11496  climcau  11531  climcaucn  11535  modfsummod  11642  p1modz1  11978  dvdsdivcl  12034  ltoddhalfle  12077  halfleoddlt  12078  ndvdssub  12114  dfgcd2  12208  coprmdvds1  12286  coprmdvds  12287  coprmdvds2  12288  divgcdcoprm0  12296  cncongr1  12298  cncongr2  12299  prmfac1  12347  pcqcl  12502  dvdsprmpweqle  12533  oddprmdvds  12550  prmpwdvds  12551  infpnlem1  12555  lidrididd  13086  mulgaddcom  13354  mulginvcom  13355  imasabl  13544  lmodfopnelem1  13958  lss1d  14017  rnglidlmcl  14114  znrrg  14294  uniopn  14345  tgcnp  14553  iscnp4  14562  lmtopcnp  14594  txlm  14623  metss  14838  metcnp3  14855  logbgcd1irr  15311  gausslemma2dlem1a  15407  gausslemma2dlem2  15411  gausslemma2dlem3  15412  lgsquad2lem2  15431  2lgslem1a1  15435  2sqlem6  15469  bj-rspgt  15540