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  6357  genpcdl  6617  genpcuu  6618  distrlem5prl  6684  distrlem5pru  6685  lemul12a  7828  divgt0  7838  divge0  7839  bndndx  8180  elnnz  8255  fzind  8353  fnn0ind  8354  eqreznegel  8549  lbzbi  8551  irradd  8580  irrmul  8581  ledivge1le  8652  iccid  8794  uzsubsubfz  8911  fzrevral  8967  elfz0fzfz0  8983  fz0fzelfz0  8984  elfzmlbp  8990  elfzodifsumelfzo  9057  ssfzo12bi  9081  elfzonelfzo  9086  flqeqceilz  9160  le2sq2  9329  cau3lem  9710  mulcn2  9833  climcau  9866  climcaucn  9870  bj-rspgt  9925