Theorem com23 72

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	⊢ (φ → (ψ → (χ → θ)))

Assertion

Ref	Expression
com23	⊢ (φ → (χ → (ψ → θ)))

Proof of Theorem com23

Step	Hyp	Ref	Expression
1		com3.1	. 2 ⊢ (φ → (ψ → (χ → θ)))
2		pm2.27 35	. 2 ⊢ (χ → ((χ → θ) → θ))
3	1, 2	syl9 66	1 ⊢ (φ → (χ → (ψ → θ)))

Syntax hints:   → wi 4

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7

This theorem is referenced by:  com3r  73  com13  74  pm2.04  76  pm2.86d  93  impancom  247  con2d  554  impidc  754  pm2.61dc  761  3com23  1109  expcomd  1327  spimth  1620  sbiedh  1667  eqrdav  2036  necon4bbiddc  2273  ralrimdva  2393  ralrimdvva  2398  ceqsalt  2574  vtoclgft  2598  reu6  2724  sbciegft  2787  reuss2  3211  reupick  3215  reusv3  4158  ssrel  4371  ssrel2  4373  ssrelrel  4383  funssres  4885  funcnvuni  4911  fv3  5140  fvmptt  5205  funfvima2  5334  isoini  5400  isopolem  5404  f1ocnv2d  5646  f1o2ndf1  5791  nnmordi  6025  nnmord  6026  xpdom2  6241  genpcdl  6501  genpcuu  6502  distrlem5prl  6561  distrlem5pru  6562  lemul12a  7589  divgt0  7599  divge0  7600  bndndx  7936  elnnz  8011  fzind  8109  fnn0ind  8110  eqreznegel  8305  lbzbi  8307  irradd  8335  irrmul  8336  iccid  8544  uzsubsubfz  8661  fzrevral  8717  elfz0fzfz0  8733  fz0fzelfz0  8734  elfzmlbp  8740  elfzodifsumelfzo  8807  ssfzo12bi  8831  elfzonelfzo  8836  le2sq2  8962  bj-rspgt  9240