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  755  pm2.61dc  762  3com23  1110  expcomd  1330  spimth  1623  sbiedh  1670  eqrdav  2039  necon4bbiddc  2279  ralrimdva  2399  ralrimdvva  2404  ceqsalt  2580  vtoclgft  2604  reu6  2730  sbciegft  2793  reuss2  3217  reupick  3221  reusv3  4192  ssrel  4428  ssrel2  4430  ssrelrel  4440  funssres  4942  funcnvuni  4968  fv3  5197  fvmptt  5262  funfvima2  5391  isoini  5457  isopolem  5461  f1ocnv2d  5704  f1o2ndf1  5849  nnmordi  6089  nnmord  6090  xpdom2  6305  findcard2  6346  findcard2s  6347  findcard2d  6348  findcard2sd  6349  ordiso2  6355  genpcdl  6615  genpcuu  6616  distrlem5prl  6682  distrlem5pru  6683  lemul12a  7826  divgt0  7836  divge0  7837  bndndx  8178  elnnz  8253  fzind  8351  fnn0ind  8352  eqreznegel  8547  lbzbi  8549  irradd  8578  irrmul  8579  ledivge1le  8650  iccid  8792  uzsubsubfz  8909  fzrevral  8965  elfz0fzfz0  8981  fz0fzelfz0  8982  elfzmlbp  8988  elfzodifsumelfzo  9055  ssfzo12bi  9079  elfzonelfzo  9084  flqeqceilz  9158  le2sq2  9303  cau3lem  9684  mulcn2  9807  climcau  9840  climcaucn  9844  bj-rspgt  9899