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  100  impcomd  255  impancom  260  a2and  560  con2d  629  impidc  866  pm2.61dc  873  3com23  1236  expcomd  1487  spimth  1783  sbiedh  1835  eqrdav  2230  necon4bbiddc  2477  ralrimdva  2613  ralrimdvva  2618  ceqsalt  2830  vtoclgft  2855  reu6  2996  sbciegft  3063  reuss2  3489  reupick  3493  reusv3  4563  ssrel  4820  ssrel2  4822  ssrelrel  4832  ssrelrn  4928  funssres  5376  funcnvuni  5406  f1ssf1  5624  fv3  5671  fvmptt  5747  funfvima2  5897  isoini  5969  isopolem  5973  f1ocnv2d  6237  f1o2ndf1  6402  suppfnss  6435  suppssdc  6438  nnmordi  6727  nnmord  6728  xpdom2  7058  findcard2  7121  findcard2s  7122  findcard2d  7123  findcard2sd  7124  xpfi  7167  ordiso2  7277  updjud  7324  genpcdl  7782  genpcuu  7783  distrlem5prl  7849  distrlem5pru  7850  lemul12a  9085  divgt0  9095  divge0  9096  lbreu  9168  bndndx  9444  elnnz  9532  nzadd  9575  fzind  9638  fnn0ind  9639  eqreznegel  9891  lbzbi  9893  irradd  9923  irrmul  9924  ledivge1le  10004  iccid  10203  uzsubsubfz  10325  fzrevral  10383  elfz0fzfz0  10404  fz0fzelfz0  10405  elfzmlbp  10410  elincfzoext  10482  elfzodifsumelfzo  10490  ssfzo12bi  10514  elfzonelfzo  10519  flqeqceilz  10624  le2sq2  10921  facdiv  11044  facwordi  11046  faclbnd  11047  fundm2domnop0  11156  swrdswrdlem  11332  swrdswrd  11333  ccatopth2  11345  wrd2ind  11351  pfxccatin12lem2a  11355  swrdccatin2  11357  pfxccatin12lem2  11359  pfxccatin12lem3  11360  swrdccat  11363  swrdccat3blem  11367  reuccatpfxs1lem  11374  cau3lem  11735  mulcn2  11933  climcau  11968  climcaucn  11972  modfsummod  12080  p1modz1  12416  dvdsdivcl  12472  ltoddhalfle  12515  halfleoddlt  12516  ndvdssub  12552  dfgcd2  12646  coprmdvds1  12724  coprmdvds  12725  coprmdvds2  12726  divgcdcoprm0  12734  cncongr1  12736  cncongr2  12737  prmfac1  12785  pcqcl  12940  dvdsprmpweqle  12971  oddprmdvds  12988  prmpwdvds  12989  infpnlem1  12993  lidrididd  13526  mulgaddcom  13794  mulginvcom  13795  imasabl  13984  lmodfopnelem1  14400  lss1d  14459  rnglidlmcl  14556  znrrg  14736  uniopn  14792  tgcnp  15000  iscnp4  15009  lmtopcnp  15041  txlm  15070  metss  15285  metcnp3  15302  logbgcd1irr  15758  gausslemma2dlem1a  15857  gausslemma2dlem2  15861  gausslemma2dlem3  15862  lgsquad2lem2  15881  2lgslem1a1  15885  2sqlem6  15919  umgrnloop  16037  upgredgpr  16070  usgrausgrben  16093  usgredg2vlem2  16144  ushgredgedg  16147  ushgredgedgloop  16149  wlk1walkdom  16280  uspgr2wlkeqi  16288  clwwlk1loop  16320  clwwlkccatlem  16321  umgrclwwlkge2  16323  clwwlknonex2lem2  16359  clwwlknonex2  16360  bj-rspgt  16484  gfsumval  16789