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  1188  expcomd  1418  spimth  1714  sbiedh  1761  eqrdav  2139  necon4bbiddc  2383  ralrimdva  2515  ralrimdvva  2520  ceqsalt  2715  vtoclgft  2739  reu6  2877  sbciegft  2943  reuss2  3361  reupick  3365  reusv3  4389  ssrel  4635  ssrel2  4637  ssrelrel  4647  funssres  5173  funcnvuni  5200  fv3  5452  fvmptt  5520  funfvima2  5658  isoini  5727  isopolem  5731  f1ocnv2d  5982  f1o2ndf1  6133  nnmordi  6420  nnmord  6421  xpdom2  6733  findcard2  6791  findcard2s  6792  findcard2d  6793  findcard2sd  6794  xpfi  6826  ordiso2  6928  updjud  6975  genpcdl  7351  genpcuu  7352  distrlem5prl  7418  distrlem5pru  7419  lemul12a  8644  divgt0  8654  divge0  8655  lbreu  8727  bndndx  9000  elnnz  9088  nzadd  9130  fzind  9190  fnn0ind  9191  eqreznegel  9433  lbzbi  9435  irradd  9465  irrmul  9466  ledivge1le  9543  iccid  9738  uzsubsubfz  9858  fzrevral  9916  elfz0fzfz0  9934  fz0fzelfz0  9935  elfzmlbp  9940  elfzodifsumelfzo  10009  ssfzo12bi  10033  elfzonelfzo  10038  flqeqceilz  10122  le2sq2  10399  facdiv  10516  facwordi  10518  faclbnd  10519  cau3lem  10918  mulcn2  11113  climcau  11148  climcaucn  11152  modfsummod  11259  dvdsdivcl  11584  ltoddhalfle  11626  halfleoddlt  11627  ndvdssub  11663  dfgcd2  11738  coprmdvds1  11808  coprmdvds  11809  coprmdvds2  11810  divgcdcoprm0  11818  cncongr1  11820  cncongr2  11821  prmfac1  11866  uniopn  12207  tgcnp  12417  iscnp4  12426  lmtopcnp  12458  txlm  12487  metss  12702  metcnp3  12719  logbgcd1irr  13092  bj-rspgt  13164