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  560  con2d  629  impidc  866  pm2.61dc  873  3com23  1236  expcomd  1487  spimth  1783  sbiedh  1835  eqrdav  2230  necon4bbiddc  2477  ralrimdva  2613  ralrimdvva  2618  ceqsalt  2830  vtoclgft  2855  reu6  2996  sbciegft  3063  reuss2  3489  reupick  3493  reusv3  4563  ssrel  4820  ssrel2  4822  ssrelrel  4832  ssrelrn  4928  funssres  5376  funcnvuni  5406  f1ssf1  5624  fv3  5671  fvmptt  5747  funfvima2  5897  isoini  5969  isopolem  5973  f1ocnv2d  6237  f1o2ndf1  6402  suppfnss  6435  suppssdc  6438  nnmordi  6727  nnmord  6728  xpdom2  7058  findcard2  7121  findcard2s  7122  findcard2d  7123  findcard2sd  7124  xpfi  7167  ordiso2  7294  updjud  7341  genpcdl  7799  genpcuu  7800  distrlem5prl  7866  distrlem5pru  7867  lemul12a  9101  divgt0  9111  divge0  9112  lbreu  9184  bndndx  9460  elnnz  9550  nzadd  9593  fzind  9656  fnn0ind  9657  eqreznegel  9909  lbzbi  9911  irradd  9941  irrmul  9942  ledivge1le  10022  iccid  10221  uzsubsubfz  10344  fzrevral  10402  elfz0fzfz0  10423  fz0fzelfz0  10424  elfzmlbp  10429  elincfzoext  10501  elfzodifsumelfzo  10509  ssfzo12bi  10533  elfzonelfzo  10538  flqeqceilz  10643  le2sq2  10940  facdiv  11063  facwordi  11065  faclbnd  11066  fundm2domnop0  11175  swrdswrdlem  11351  swrdswrd  11352  ccatopth2  11364  wrd2ind  11370  pfxccatin12lem2a  11374  swrdccatin2  11376  pfxccatin12lem2  11378  pfxccatin12lem3  11379  swrdccat  11382  swrdccat3blem  11386  reuccatpfxs1lem  11393  cau3lem  11754  mulcn2  11952  climcau  11987  climcaucn  11991  modfsummod  12099  p1modz1  12435  dvdsdivcl  12491  ltoddhalfle  12534  halfleoddlt  12535  ndvdssub  12571  dfgcd2  12665  coprmdvds1  12743  coprmdvds  12744  coprmdvds2  12745  divgcdcoprm0  12753  cncongr1  12755  cncongr2  12756  prmfac1  12804  pcqcl  12959  dvdsprmpweqle  12990  oddprmdvds  13007  prmpwdvds  13008  infpnlem1  13012  lidrididd  13545  mulgaddcom  13813  mulginvcom  13814  imasabl  14003  lmodfopnelem1  14420  lss1d  14479  rnglidlmcl  14576  znrrg  14756  uniopn  14812  tgcnp  15020  iscnp4  15029  lmtopcnp  15061  txlm  15090  metss  15305  metcnp3  15322  logbgcd1irr  15778  gausslemma2dlem1a  15877  gausslemma2dlem2  15881  gausslemma2dlem3  15882  lgsquad2lem2  15901  2lgslem1a1  15905  2sqlem6  15939  umgrnloop  16057  upgredgpr  16090  usgrausgrben  16113  usgredg2vlem2  16164  ushgredgedg  16167  ushgredgedgloop  16169  wlk1walkdom  16300  uspgr2wlkeqi  16308  clwwlk1loop  16340  clwwlkccatlem  16341  umgrclwwlkge2  16343  clwwlknonex2lem2  16379  clwwlknonex2  16380  bj-rspgt  16504  gfsumval  16809