Theorem com23 87

Description: Commutation of antecedents. Swap 2nd and 3rd. Deduction associated with com12 33. (Contributed by NM, 27-Dec-1992.) (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 43	. 2 ⊢ (𝜒 → ((𝜒 → 𝜃) → 𝜃))
3	1, 2	syl9 78	1 ⊢ (𝜑 → (𝜒 → (𝜓 → 𝜃)))

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  com3r  88  com13  89  pm2.04  91  pm2.86d  109  impcomd  417  expcomd  422  impancom  457  a2and  859  dedlem0b  1060  sbequ1  2283  moexexlem  2651  ralrimdvva  3217  ceqsal1t  3482  ceqsalt  3483  spcimgft  3510  vtoclgft  3515  elabgtOLD  3627  reupick  4275  reusv3  5370  sbcop1  5464  propeqop  5484  pwssun  5547  wefrc  5649  ssrel  5763  ssrel2  5765  ssrelrel  5776  ssrelrn  5878  tz7.7  6383  ordtr2  6403  onmindif  6452  unizlim  6482  funssres  6577  f1ssf1  6850  fvmptt  7007  fveqdmss  7071  fvcofneq  7086  funsndifnop  7148  funfvima2  7230  isoini  7339  isopolem  7346  weniso  7357  f1ocnv2d  7667  limsssuc  7846  tfindsg  7857  limomss  7867  findsg  7894  funcnvuni  7929  f1oweALT  7969  funelss  8044  bropopvvv  8087  bropfvvvvlem  8088  bropfvvvv  8089  f1o2ndf1  8119  frxp  8124  soseq  8157  suppfnss  8187  onfununi  8330  tz7.49  8434  omordi  8553  omlimcl  8565  omass  8567  oeordsuc  8582  nnmordi  8619  nnmord  8620  omabs  8639  xpdom2  9070  infensuc  9153  findcard2  9159  findcard2d  9161  findcard3  9253  frfi  9255  fsuppres  9363  dffi2  9393  elfiun  9400  ordiso2  9487  ordtypelem7  9496  suc11reg  9598  inf3lem2  9608  noinfep  9639  cantnfle  9650  cantnflem1  9668  cantnf  9672  ttrclss  9699  trcl  9707  epfrs  9710  frr3g  9738  r1sdom  9756  updjud  9939  dfac8alem  10032  indcardi  10044  alephordi  10077  dfac12lem3  10148  pwsdompw  10205  cofsmo  10271  cfcoflem  10274  coftr  10275  isf32lem2  10356  isf32lem9  10363  axcc3  10440  domtriomlem  10444  axdc3lem2  10453  axdc3lem4  10455  zorn2lem4  10501  zorn2lem6  10503  zorn2lem7  10504  ttukeylem6  10516  uniimadom  10552  konigthlem  10577  fpwwe2lem7  10646  tskord  10789  tskcard  10790  grupr  10806  gruiin  10819  grudomon  10826  grur1a  10828  genpn0  11012  genpcd  11015  distrlem5pr  11036  psslinpr  11040  ltaddpr  11043  ltexprlem3  11047  ltexprlem6  11050  ltapr  11054  prlem936  11056  suplem1pr  11061  axpre-sup  11178  1re  11232  dedekindle  11398  lemul12a  12097  divgt0  12107  divge0  12108  lbreu  12189  sup2  12195  bndndx  12527  elnnz  12625  nzadd  12666  fzind  12719  fnn0ind  12720  uzwo  12960  lbzbi  12985  zmax  12994  zbtwnre  12995  irradd  13023  irrmul  13024  ledivge1le  13115  xrub  13364  supxrunb2  13372  infmremnf  13396  iccid  13443  uzsubsubfz  13601  fzrevral  13667  elfz0fzfz0  13688  fz0fzelfz0  13689  elfzmlbp  13694  elincfzoext  13779  ssfzoulel  13816  ssfzo12bi  13817  fzoopth  13818  elfzonelfzo  13825  elfznelfzo  13829  elfznelfzob  13830  injresinjlem  13846  fleqceilz  13915  modaddmodup  13998  uzindi  14046  suppssfz  14058  mptnn0fsuppr  14063  le2sq2  14199  sqlecan  14273  facdiv  14351  facwordi  14353  faclbnd  14354  hashimarni  14506  hash2prd  14540  hashle2pr  14542  pr2pwpr  14544  fundmge2nop0  14567  fi1uzind  14572  brfi1indALT  14575  swrdnd2  14725  swrdnnn0nd  14726  swrdnd0  14727  pfxnd0  14758  swrdswrdlem  14773  swrdswrd  14774  ccatopth2  14786  wrd2ind  14792  pfxccatin12lem2a  14796  swrdccatin2  14798  pfxccatin12lem2  14800  pfxccatin12lem3  14801  swrdccat  14804  swrdccat3blem  14808  reuccatpfxs1lem  14815  repswswrd  14855  cshwidxmod  14874  cshwidx0  14877  2cshwcshw  14896  cshwcsh2id  14899  cau3lem  15442  caubnd  15446  climrlim2  15634  rlimcn3  15677  mulcn2  15683  climcau  15758  climbdd  15759  caucvg  15766  modfsummod  15881  p1modz1  16349  dvdsle  16400  dvdsdivcl  16406  ltoddhalfle  16451  halfleoddlt  16452  ndvdssub  16499  gcdcllem1  16589  dvdslegcd  16594  bezoutlem4  16632  dfgcd2  16636  lcmf  16723  lcmfunsnlem1  16727  lcmfunsnlem2lem1  16728  lcmfunsnlem  16731  lcmfdvdsb  16733  lcmfun  16735  coprmdvds1  16742  divgcdcoprm0  16755  cncongr1  16757  cncongr2  16758  prmfac1  16811  pcqcl  16948  dvdsprmpweqle  16978  oddprmdvds  16995  prmpwdvds  16996  infpnlem1  17002  prmgaplem5  17147  prmgaplem6  17148  prmgaplem7  17149  cshwshashlem1  17187  cictr  17894  initoeu2lem1  18103  initoeu2  18105  clatleglb  18606  lidrididd  18764  mulgaddcom  19221  mulginvcom  19222  cycsubm  19330  cyccom  19331  gsmsymgreqlem2  19558  symggen  19597  psgnunilem4  19624  sylow2blem3  19749  frgpnabllem1  20000  imasabl  20003  dprddisj2  20168  lmodfopnelem1  21082  lssssr  21138  lss1d  21147  lspsncv0  21333  rnglidlmcl  21404  lidlunin0  21424  unichnlidl  21425  rngqiprngimfo  21504  nzerooringczr  21693  pzriprnglem5  21698  pzriprnglem8  21701  znrrg  21778  mplcoe5lem  22255  cply1mul  22521  coe1fzgsumdlem  22528  gsummoncoe1  22533  evl1gsumdlem  22581  mamufacex  22618  dmatelnd  22718  scmataddcl  22738  scmatsubcl  22739  scmatmulcl  22740  smatvscl  22746  mavmulsolcl  22773  mdetdiagid  22822  matunitlindflem1  22901  matunitlindflem2  22902  cramerlem3  22914  pmatcoe1fsupp  22926  cpmatacl  22941  cpmatmcllem  22943  mp2pm2mplem4  23034  chpscmat  23067  chfacfisf  23079  chfacfisfcpmat  23080  uniopn  23122  opnnei  23345  neindisj2  23348  restcls  23406  restntr  23407  tgcnp  23478  subbascn  23479  iscnp4  23488  lpcls  23589  cmpsublem  23624  cmpsub  23625  tgcmp  23626  cmpcld  23627  dfconn2  23644  1stcrest  23678  2ndcdisj  23682  1stccnp  23688  comppfsc  23758  kgencn2  23783  txlm  23874  kqreglem1  23967  filin  24080  isfil2  24082  ufilmax  24133  ufileu  24145  filufint  24146  cfinufil  24154  elfm2  24174  rnelfmlem  24178  rnelfm  24179  flimopn  24201  fbflim2  24203  flffbas  24221  fclsnei  24245  flimfnfcls  24254  fclscmp  24256  fcfnei  24261  cnpfcf  24267  alexsubALTlem2  24274  alexsubALTlem3  24275  alexsubALTlem4  24276  alexsubALT  24277  ptcmplem4  24281  qustgplem  24347  tsmsres  24370  tsmsxp  24381  metss  24734  metcnp3  24766  ovoliunnul  25735  ovolicc2lem3  25747  dyadmax  25826  itg2le  25967  bddiblnc  26069  itgcn  26072  ellimc3  26106  lhop1  26241  dvfsumrlim  26258  fta1g  26395  dvply2g  26515  fta1  26538  aalioulem3  26570  aalioulem4  26571  ulmcaulem  26630  ulmcau  26631  logbgcd1irr  27031  xrlimcnp  27205  cxploglim  27214  jensen  27225  lgsqrmodndvds  27589  gausslemma2dlem1a  27601  gausslemma2dlem2  27603  gausslemma2dlem3  27604  lgsquad2lem2  27621  2lgslem1a1  27625  2sqlem6  27659  2sq2  27669  2sqnn  27675  2sqreultblem  27684  nosepdmlem  27919  nodenselem8  27927  eqcuts3  28069  madebdaylemlrcut  28164  addsprop  28241  addsuniflem  28266  negsprop  28300  mulsprop  28395  mulsuniflem  28414  precsex  28483  onsfi  28621  elnnzs  28666  elreno2  28760  brbtwn2  29362  ax5seglem5  29390  axcontlem4  29424  axcontlem10  29430  umgrnloopv  29563  umgrnloop  29565  upgredgpr  29599  numedglnl  29601  usgrausgrb  29629  usgrnloopvALT  29661  usgrnloopALT  29663  usgredg2vlem2  29686  ushgredgedg  29689  ushgredgedgloop  29691  upgrreslem  29764  umgrreslem  29765  nbgr0edglem  29816  nbusgrvtxm1  29839  uvtxnbgrvtx  29853  cusgredg  29884  cusgrres  29908  cusgrsize2inds  29913  cusgrfi  29918  fusgrregdegfi  30029  ewlkle  30065  uspgr2wlkeqi  30107  lfgrwlkprop  30149  lfgrwlknloop  30151  pthdivtx  30191  2pthnloop  30196  upgrwlkdvdelem  30201  upgrspthswlk  30203  usgr2wlkneq  30221  usgr2trlncl  30225  usgr2pthlem  30228  usgr2pth  30229  uspgrn2crct  30276  crctcshwlkn0lem4  30281  crctcshwlkn0lem5  30282  crctcshwlkn0  30289  wlkiswwlks1  30335  wlkiswwlks2  30343  wlkiswwlksupgr2  30345  wwlksnred  30360  wwlksnext  30361  wwlksnextbi  30362  wwlksnextwrd  30365  wwlksnextinj  30367  wwlksnextproplem2  30378  wwlksnextproplem3  30379  wspthsnonn0vne  30385  wspn0  30392  2pthon3v  30411  usgrwwlks2on  30426  umgrwwlks2on  30427  elwspths2on  30430  elwspths2onw  30431  wpthswwlks2on  30432  clwwlk1loop  30458  clwwlkccatlem  30459  umgrclwwlkge2  30461  clwlkclwwlklem2a4  30467  clwlkclwwlklem2a  30468  clwlkclwwlklem3  30471  clwlkclwwlkf1lem3  30476  clwlkclwwlkfo  30479  clwwisshclwwslemlem  30483  erclwwlkeqlen  30489  erclwwlksym  30491  clwwlkf  30517  clwwlknscsh  30532  erclwwlknsym  30540  clwwlknonex2lem2  30578  clwwlknonex2  30579  umgr2cycllem  30625  upgr3v3e3cycl  30660  upgr4cycl4dv4e  30665  eucrctshift  30723  3vfriswmgr  30758  1to2vfriswmgr  30759  1to3vfriswmgr  30760  n4cyclfrgr  30771  4cyclusnfrgr  30772  frgrnbnb  30773  frgrncvvdeqlem8  30786  frgrwopreg  30803  frgr2wwlk1  30809  frgr2wwlkeqm  30811  2clwwlk2clwwlklem  30826  numclwwlk1lem2fo  30838  wlkl0  30847  numclwlk2lem2f  30857  frgrreggt1  30873  frgrreg  30874  frgrregord013  30875  frgrregord13  30876  frgrogt3nreg  30877  eulplig  30966  nmoub3i  31254  ipasslem5  31316  htthlem  31398  ocin  31777  spansneleq  32051  spansnss  32052  elspansn4  32054  h1datomi  32062  nmopub2tALT  32390  nmfnleub2  32407  hstel2  32700  cvnbtwn  32767  spansncv2  32774  dmdmd  32781  dmdbr3  32786  dmdbr4  32787  dmdbr5  32789  mdsl0  32791  mdexchi  32816  cvexchlem  32849  atcv1  32861  atomli  32863  atcvatlem  32866  atcvat2i  32868  chirredi  32875  mdsymlem3  32886  mdsymlem4  32887  sumdmdii  32896  sumdmdlem  32899  cdj1i  32914  ssrelf  33088  f1o3d  33099  fisshasheq  35717  cvxpconn  35821  satfv0  35937  satfsschain  35943  satfrel  35946  satfdm  35948  satfv0fun  35950  sat1el2xp  35958  gonarlem  35973  goalrlem  35975  satffunlem1lem1  35981  satffunlem2lem1  35983  satffunlem2lem2  35985  satffun  35988  mrsubccat  36097  msubvrs  36139  fundmpss  36346  dfon2lem6  36365  dfon2lem8  36367  dfon2lem9  36368  dfon2  36369  wzel  36401  colinearxfr  36655  btwnconn1lem11  36677  lineintmo  36737  in-ax8  36844  ss-ax8  36845  trer  36935  elicc3  36936  finminlem  36937  nn0prpwlem  36941  fnessref  36976  neibastop2  36980  fgmin  36989  tailfb  36996  ordcmp  37066  ee7.2aOLD  37080  dfttc4  37149  bj-ceqsalt0  37627  bj-ceqsalt1  37628  isbasisrelowllem1  38109  isbasisrelowllem2  38110  relowlpssretop  38118  fvineqsneu  38165  fvineqsneq  38166  wl-mo3t  38339  finixpnum  38359  poimirlem26  38395  poimirlem27  38396  poimirlem29  38398  ftc1anc  38450  fdc  38495  heibor1lem  38559  ghomco  38641  rngoueqz  38690  unichnidl  38781  dmncan1  38826  ax12indn  39816  lshpdisj  39860  lub0N  40062  glb0N  40066  leat2  40167  hlrelat2  40276  cvrexchlem  40292  cvratlem  40294  atcvrj0  40301  cvrat2  40302  snatpsubN  40623  linepsubN  40625  pmaple  40634  pmapsub  40641  elpaddn0  40673  paddasslem5  40697  trlval2  41036  cdlemn11pre  42083  dihord2pre  42098  mapdordlem2  42510  sn-sup2  43379  fsuppind  43436  pell1qrgap  43715  dford3lem1  43867  hbtlem5  43969  onexlimgt  44084  onsucf1olem  44111  omcl2  44174  tfsconcat0b  44187  ntrneiiso  44931  sbiota1  45258  19.41rg  45373  ee223  45457  or2expropbilem1  47920  funressnfv  47931  fcoresf1  47957  2reuimp  48003  f1oresf1o2  48179  zm1nn  48190  nltle2tri  48201  el1fzopredsuc  48214  modlt0b  48257  mod2addne  48258  muldvdsfacgt  48274  muldvdsfacm1  48275  elsetpreimafvssdm  48286  imasetpreimafvbijlemf1  48304  iccpartlt  48324  iccpartgt  48327  iccelpart  48333  icceuelpart  48336  iccpartnel  48338  fargshiftfo  48342  fargshiftfva  48343  lswn0  48344  ich2exprop  48371  prsprel  48387  sprsymrelfolem2  48393  sprsymrelfo  48397  poprelb  48424  reuopreuprim  48426  goldbachthlem2  48449  odz2prm2pw  48466  fmtnoprmfac1  48468  fmtnofac2lem  48471  prmdvdsfmtnof1lem2  48488  2pwp1prm  48492  sfprmdvdsmersenne  48506  lighneallem3  48510  requad01  48537  requad2  48539  even3prm2  48635  fppr2odd  48647  fpprwpprb  48656  gbegt5  48677  sbgoldbwt  48693  sbgoldbalt  48697  sbgoldbm  48700  bgoldbtbndlem2  48722  bgoldbtbndlem3  48723  bgoldbtbndlem4  48724  bgoldbtbnd  48725  tgblthelfgott  48731  tgoldbach  48733  isubgredg  48782  grimuhgr  48803  grimcnv  48804  grimco  48805  isuspgrim0  48810  isuspgrimlem  48811  uhgrimisgrgriclem  48846  clnbgrgrimlem  48849  grimedg  48851  grtriprop  48857  cycl3grtri  48863  grimgrtri  48865  isubgr3stgrlem6  48887  uspgrlimlem3  48906  uspgrlimlem4  48907  grlimgrtrilem2  48918  grlicsym  48929  clnbgr3stgrgrlim  48935  clnbgr3stgrgrlic  48936  gpgedg2ov  48982  gpgedg2iv  48983  pgnbgreunbgrlem3  49034  pgnbgreunbgrlem6  49040  upgrwlkupwlk  49056  lmod0rng  49144  idomcanl  49262  ztprmneprm  49277  ply1mulgsumlem1  49316  ply1mulgsumlem2  49317  lcoel0  49358  linindslinci  49378  lindslinindimp2lem4  49391  lindslinindsimp2lem5  49392  snlindsntor  49401  ldepspr  49403  lincresunit2  49408  fllog2  49498  dignn0ldlem  49532  dignn0flhalflem1  49545  nn0sumshdiglemA  49549  nn0sumshdiglemB  49550  itcovalt2  49607  resum2sqorgt0  49639  eenglngeehlnmlem2  49668  rrx2linest  49672  itscnhlc0xyqsol  49695  itsclc0  49701  setrec1lem2  50614  aacllem  50772