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  564  con2d  633  impidc  870  pm2.61dc  877  3com23  1240  expcomd  1491  spimth  1788  sbiedh  1840  eqrdav  2237  necon4bbiddc  2494  ralrimdva  2630  ralrimdvva  2635  ceqsalt  2848  vtoclgft  2873  reu6  3015  sbciegft  3082  reuss2  3513  reupick  3517  reusv3  4601  ssrel  4858  ssrel2  4860  ssrelrel  4870  ssrelrn  4967  funssres  5415  funcnvuni  5445  f1ssf1  5666  fv3  5713  fvmptt  5791  funfvima2  5941  isoini  6014  isopolem  6018  f1ocnv2d  6284  f1o3d  6288  f1o2ndf1  6454  suppfnss  6487  suppssdc  6490  nnmordi  6779  nnmord  6780  xpdom2  7119  findcard2  7183  findcard2s  7184  findcard2d  7185  findcard2sd  7186  xpfi  7229  ordiso2  7365  updjud  7412  genpcdl  7876  genpcuu  7877  distrlem5prl  7943  distrlem5pru  7944  lemul12a  9182  divgt0  9192  divge0  9193  lbreu  9265  bndndx  9541  elnnz  9633  nzadd  9676  fzind  9740  fnn0ind  9741  eqreznegel  9993  lbzbi  9995  irradd  10025  irrmul  10026  ledivge1le  10106  iccid  10306  uzsubsubfz  10430  fzrevral  10490  elfz0fzfz0  10511  fz0fzelfz0  10512  elfzmlbp  10517  elincfzoext  10589  elfzodifsumelfzo  10597  ssfzo12bi  10621  elfzonelfzo  10626  flqeqceilz  10733  le2sq2  11030  facdiv  11154  facwordi  11156  faclbnd  11157  fundm2domnop0  11278  swrdswrdlem  11454  swrdswrd  11455  ccatopth2  11467  wrd2ind  11473  pfxccatin12lem2a  11477  swrdccatin2  11479  pfxccatin12lem2  11481  pfxccatin12lem3  11482  swrdccat  11485  swrdccat3blem  11489  reuccatpfxs1lem  11496  cau3lem  11858  mulcn2  12056  climcau  12091  climcaucn  12095  modfsummod  12203  p1modz1  12539  dvdsdivcl  12595  ltoddhalfle  12638  halfleoddlt  12639  ndvdssub  12675  dfgcd2  12769  coprmdvds1  12847  coprmdvds  12848  coprmdvds2  12849  divgcdcoprm0  12857  cncongr1  12859  cncongr2  12860  prmfac1  12908  pcqcl  13063  dvdsprmpweqle  13094  oddprmdvds  13111  prmpwdvds  13112  infpnlem1  13116  lidrididd  13679  mulgaddcom  13926  mulginvcom  13927  imasabl  14117  gsumvalfi  14129  lmodfopnelem1  14633  lss1d  14692  rnglidlmcl  14789  znrrg  14967  uniopn  15025  tgcnp  15233  iscnp4  15242  lmtopcnp  15274  txlm  15303  metss  15518  metcnp3  15535  logbgcd1irr  15992  gausslemma2dlem1a  16091  gausslemma2dlem2  16095  gausslemma2dlem3  16096  lgsquad2lem2  16115  2lgslem1a1  16119  2sqlem6  16153  umgrnloop  16271  upgredgpr  16304  usgrausgrben  16327  usgredg2vlem2  16378  ushgredgedg  16381  ushgredgedgloop  16383  wlk1walkdom  16514  uspgr2wlkeqi  16522  clwwlk1loop  16554  clwwlkccatlem  16555  umgrclwwlkge2  16557  clwwlknonex2lem2  16593  clwwlknonex2  16594  lealltlt2  16666  bj-rspgt  16728