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  4508  ssrel  4764  ssrel2  4766  ssrelrel  4776  funssres  5314  funcnvuni  5344  fv3  5601  fvmptt  5673  funfvima2  5819  isoini  5889  isopolem  5893  f1ocnv2d  6152  f1o2ndf1  6316  nnmordi  6604  nnmord  6605  xpdom2  6928  findcard2  6988  findcard2s  6989  findcard2d  6990  findcard2sd  6991  xpfi  7031  ordiso2  7139  updjud  7186  genpcdl  7634  genpcuu  7635  distrlem5prl  7701  distrlem5pru  7702  lemul12a  8937  divgt0  8947  divge0  8948  lbreu  9020  bndndx  9296  elnnz  9384  nzadd  9427  fzind  9490  fnn0ind  9491  eqreznegel  9737  lbzbi  9739  irradd  9769  irrmul  9770  ledivge1le  9850  iccid  10049  uzsubsubfz  10171  fzrevral  10229  elfz0fzfz0  10250  fz0fzelfz0  10251  elfzmlbp  10256  elincfzoext  10324  elfzodifsumelfzo  10332  ssfzo12bi  10356  elfzonelfzo  10361  flqeqceilz  10465  le2sq2  10762  facdiv  10885  facwordi  10887  faclbnd  10888  fundm2domnop0  10992  cau3lem  11458  mulcn2  11656  climcau  11691  climcaucn  11695  modfsummod  11802  p1modz1  12138  dvdsdivcl  12194  ltoddhalfle  12237  halfleoddlt  12238  ndvdssub  12274  dfgcd2  12368  coprmdvds1  12446  coprmdvds  12447  coprmdvds2  12448  divgcdcoprm0  12456  cncongr1  12458  cncongr2  12459  prmfac1  12507  pcqcl  12662  dvdsprmpweqle  12693  oddprmdvds  12710  prmpwdvds  12711  infpnlem1  12715  lidrididd  13247  mulgaddcom  13515  mulginvcom  13516  imasabl  13705  lmodfopnelem1  14119  lss1d  14178  rnglidlmcl  14275  znrrg  14455  uniopn  14506  tgcnp  14714  iscnp4  14723  lmtopcnp  14755  txlm  14784  metss  14999  metcnp3  15016  logbgcd1irr  15472  gausslemma2dlem1a  15568  gausslemma2dlem2  15572  gausslemma2dlem3  15573  lgsquad2lem2  15592  2lgslem1a1  15596  2sqlem6  15630  bj-rspgt  15759