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	⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))

Assertion

Ref	Expression
com23	⊢ (𝜑 → (𝜒 → (𝜓 → 𝜃)))

Proof of Theorem com23

Step	Hyp	Ref	Expression
1		com3.1	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
2		pm2.27 40	. 2 ⊢ (𝜒 → ((𝜒 → 𝜃) → 𝜃))
3	1, 2	syl9 72	1 ⊢ (𝜑 → (𝜒 → (𝜓 → 𝜃)))

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  548  con2d  614  impidc  844  pm2.61dc  851  3com23  1191  expcomd  1421  spimth  1715  sbiedh  1767  eqrdav  2156  necon4bbiddc  2401  ralrimdva  2537  ralrimdvva  2542  ceqsalt  2738  vtoclgft  2762  reu6  2901  sbciegft  2967  reuss2  3387  reupick  3391  reusv3  4419  ssrel  4673  ssrel2  4675  ssrelrel  4685  funssres  5211  funcnvuni  5238  fv3  5490  fvmptt  5558  funfvima2  5696  isoini  5765  isopolem  5769  f1ocnv2d  6021  f1o2ndf1  6172  nnmordi  6460  nnmord  6461  xpdom2  6773  findcard2  6831  findcard2s  6832  findcard2d  6833  findcard2sd  6834  xpfi  6871  ordiso2  6973  updjud  7020  genpcdl  7433  genpcuu  7434  distrlem5prl  7500  distrlem5pru  7501  lemul12a  8727  divgt0  8737  divge0  8738  lbreu  8810  bndndx  9083  elnnz  9171  nzadd  9213  fzind  9273  fnn0ind  9274  eqreznegel  9516  lbzbi  9518  irradd  9548  irrmul  9549  ledivge1le  9626  iccid  9822  uzsubsubfz  9942  fzrevral  10000  elfz0fzfz0  10018  fz0fzelfz0  10019  elfzmlbp  10024  elfzodifsumelfzo  10093  ssfzo12bi  10117  elfzonelfzo  10122  flqeqceilz  10210  le2sq2  10487  facdiv  10605  facwordi  10607  faclbnd  10608  cau3lem  11007  mulcn2  11202  climcau  11237  climcaucn  11241  modfsummod  11348  p1modz1  11683  dvdsdivcl  11734  ltoddhalfle  11776  halfleoddlt  11777  ndvdssub  11813  dfgcd2  11889  coprmdvds1  11959  coprmdvds  11960  coprmdvds2  11961  divgcdcoprm0  11969  cncongr1  11971  cncongr2  11972  prmfac1  12017  uniopn  12370  tgcnp  12580  iscnp4  12589  lmtopcnp  12621  txlm  12650  metss  12865  metcnp3  12882  logbgcd1irr  13255  bj-rspgt  13331