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  6502  genpcuu  6503  distrlem5prl  6562  distrlem5pru  6563  lemul12a  7609  divgt0  7619  divge0  7620  bndndx  7956  elnnz  8031  fzind  8129  fnn0ind  8130  eqreznegel  8325  lbzbi  8327  irradd  8355  irrmul  8356  iccid  8564  uzsubsubfz  8681  fzrevral  8737  elfz0fzfz0  8753  fz0fzelfz0  8754  elfzmlbp  8760  elfzodifsumelfzo  8827  ssfzo12bi  8851  elfzonelfzo  8856  le2sq2  8982  bj-rspgt  9260