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  547  con2d  613  impidc  843  pm2.61dc  850  3com23  1187  expcomd  1417  spimth  1713  sbiedh  1760  eqrdav  2138  necon4bbiddc  2382  ralrimdva  2512  ralrimdvva  2517  ceqsalt  2712  vtoclgft  2736  reu6  2873  sbciegft  2939  reuss2  3356  reupick  3360  reusv3  4381  ssrel  4627  ssrel2  4629  ssrelrel  4639  funssres  5165  funcnvuni  5192  fv3  5444  fvmptt  5512  funfvima2  5650  isoini  5719  isopolem  5723  f1ocnv2d  5974  f1o2ndf1  6125  nnmordi  6412  nnmord  6413  xpdom2  6725  findcard2  6783  findcard2s  6784  findcard2d  6785  findcard2sd  6786  xpfi  6818  ordiso2  6920  updjud  6967  genpcdl  7327  genpcuu  7328  distrlem5prl  7394  distrlem5pru  7395  lemul12a  8620  divgt0  8630  divge0  8631  lbreu  8703  bndndx  8976  elnnz  9064  nzadd  9106  fzind  9166  fnn0ind  9167  eqreznegel  9406  lbzbi  9408  irradd  9438  irrmul  9439  ledivge1le  9513  iccid  9708  uzsubsubfz  9827  fzrevral  9885  elfz0fzfz0  9903  fz0fzelfz0  9904  elfzmlbp  9909  elfzodifsumelfzo  9978  ssfzo12bi  10002  elfzonelfzo  10007  flqeqceilz  10091  le2sq2  10368  facdiv  10484  facwordi  10486  faclbnd  10487  cau3lem  10886  mulcn2  11081  climcau  11116  climcaucn  11120  modfsummod  11227  dvdsdivcl  11548  ltoddhalfle  11590  halfleoddlt  11591  ndvdssub  11627  dfgcd2  11702  coprmdvds1  11772  coprmdvds  11773  coprmdvds2  11774  divgcdcoprm0  11782  cncongr1  11784  cncongr2  11785  prmfac1  11830  uniopn  12168  tgcnp  12378  iscnp4  12387  lmtopcnp  12419  txlm  12448  metss  12663  metcnp3  12680  bj-rspgt  12993