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  6578  f1ssf1  6851  fvmptt  7008  fveqdmss  7072  fvcofneq  7087  funsndifnop  7149  funfvima2  7231  isoini  7340  isopolem  7347  weniso  7358  f1ocnv2d  7668  limsssuc  7847  tfindsg  7858  limomss  7868  findsg  7895  funcnvuni  7930  f1oweALT  7970  funelss  8045  bropopvvv  8088  bropfvvvvlem  8089  bropfvvvv  8090  f1o2ndf1  8120  frxp  8125  soseq  8158  suppfnss  8188  onfununi  8331  tz7.48lem  8432  tz7.49  8437  omordi  8556  omlimcl  8568  omass  8570  oeordsuc  8585  nnmordi  8622  nnmord  8623  omabs  8642  xpdom2  9073  infensuc  9156  findcard2  9162  findcard2d  9164  findcard3  9256  frfi  9258  fsuppres  9366  dffi2  9396  elfiun  9403  ordiso2  9490  ordtypelem7  9499  suc11reg  9601  inf3lem2  9611  noinfep  9642  cantnfle  9653  cantnflem1  9671  cantnf  9675  ttrclss  9702  trcl  9710  epfrs  9713  frr3g  9741  r1sdom  9759  updjud  9942  dfac8alem  10035  indcardi  10047  alephordi  10080  dfac12lem3  10151  pwsdompw  10208  cofsmo  10274  cfcoflem  10277  coftr  10278  isf32lem2  10359  isf32lem9  10366  axcc3  10443  domtriomlem  10447  axdc3lem2  10456  axdc3lem4  10458  zorn2lem4  10504  zorn2lem6  10506  zorn2lem7  10507  ttukeylem6  10519  uniimadom  10555  konigthlem  10580  fpwwe2lem7  10649  tskord  10792  tskcard  10793  grupr  10809  gruiin  10822  grudomon  10829  grur1a  10831  genpn0  11015  genpcd  11018  distrlem5pr  11039  psslinpr  11043  ltaddpr  11046  ltexprlem3  11050  ltexprlem6  11053  ltapr  11057  prlem936  11059  suplem1pr  11064  axpre-sup  11181  1re  11235  dedekindle  11401  lemul12a  12100  divgt0  12110  divge0  12111  lbreu  12192  sup2  12198  bndndx  12530  elnnz  12628  nzadd  12669  fzind  12722  fnn0ind  12723  uzwo  12963  lbzbi  12988  zmax  12997  zbtwnre  12998  irradd  13026  irrmul  13027  ledivge1le  13118  xrub  13367  supxrunb2  13375  infmremnf  13399  iccid  13446  uzsubsubfz  13604  fzrevral  13670  elfz0fzfz0  13691  fz0fzelfz0  13692  elfzmlbp  13697  elincfzoext  13782  ssfzoulel  13819  ssfzo12bi  13820  fzoopth  13821  elfzonelfzo  13828  elfznelfzo  13832  elfznelfzob  13833  injresinjlem  13849  fleqceilz  13918  modaddmodup  14001  uzindi  14049  suppssfz  14061  mptnn0fsuppr  14066  le2sq2  14202  sqlecan  14276  facdiv  14354  facwordi  14356  faclbnd  14357  hashimarni  14509  hash2prd  14543  hashle2pr  14545  pr2pwpr  14547  fundmge2nop0  14570  fi1uzind  14575  brfi1indALT  14578  swrdnd2  14728  swrdnnn0nd  14729  swrdnd0  14730  pfxnd0  14761  swrdswrdlem  14776  swrdswrd  14777  ccatopth2  14789  wrd2ind  14795  pfxccatin12lem2a  14799  swrdccatin2  14801  pfxccatin12lem2  14803  pfxccatin12lem3  14804  swrdccat  14807  swrdccat3blem  14811  reuccatpfxs1lem  14818  repswswrd  14858  cshwidxmod  14877  cshwidx0  14880  2cshwcshw  14899  cshwcsh2id  14902  cau3lem  15445  caubnd  15449  climrlim2  15637  rlimcn3  15680  mulcn2  15686  climcau  15761  climbdd  15762  caucvg  15769  modfsummod  15884  p1modz1  16352  dvdsle  16403  dvdsdivcl  16409  ltoddhalfle  16454  halfleoddlt  16455  ndvdssub  16502  gcdcllem1  16592  dvdslegcd  16597  bezoutlem4  16635  dfgcd2  16639  lcmf  16726  lcmfunsnlem1  16730  lcmfunsnlem2lem1  16731  lcmfunsnlem  16734  lcmfdvdsb  16736  lcmfun  16738  coprmdvds1  16745  divgcdcoprm0  16758  cncongr1  16760  cncongr2  16761  prmfac1  16814  pcqcl  16951  dvdsprmpweqle  16981  oddprmdvds  16998  prmpwdvds  16999  infpnlem1  17005  prmgaplem5  17150  prmgaplem6  17151  prmgaplem7  17152  cshwshashlem1  17190  cictr  17897  initoeu2lem1  18106  initoeu2  18108  clatleglb  18609  lidrididd  18767  mulgaddcom  19224  mulginvcom  19225  cycsubm  19333  cyccom  19334  gsmsymgreqlem2  19561  symggen  19600  psgnunilem4  19627  sylow2blem3  19752  frgpnabllem1  20003  imasabl  20006  dprddisj2  20171  lmodfopnelem1  21085  lssssr  21141  lss1d  21150  lspsncv0  21336  rnglidlmcl  21407  lidlunin0  21427  unichnlidl  21428  rngqiprngimfo  21507  nzerooringczr  21696  pzriprnglem5  21701  pzriprnglem8  21704  znrrg  21781  mplcoe5lem  22258  cply1mul  22524  coe1fzgsumdlem  22531  gsummoncoe1  22536  evl1gsumdlem  22584  mamufacex  22621  dmatelnd  22721  scmataddcl  22741  scmatsubcl  22742  scmatmulcl  22743  smatvscl  22749  mavmulsolcl  22776  mdetdiagid  22825  matunitlindflem1  22904  matunitlindflem2  22905  cramerlem3  22917  pmatcoe1fsupp  22929  cpmatacl  22944  cpmatmcllem  22946  mp2pm2mplem4  23037  chpscmat  23070  chfacfisf  23082  chfacfisfcpmat  23083  uniopn  23125  opnnei  23348  neindisj2  23351  restcls  23409  restntr  23410  tgcnp  23481  subbascn  23482  iscnp4  23491  lpcls  23592  cmpsublem  23627  cmpsub  23628  tgcmp  23629  cmpcld  23630  dfconn2  23647  1stcrest  23681  2ndcdisj  23685  1stccnp  23691  comppfsc  23761  kgencn2  23786  txlm  23877  kqreglem1  23970  filin  24083  isfil2  24085  ufilmax  24136  ufileu  24148  filufint  24149  cfinufil  24157  elfm2  24177  rnelfmlem  24181  rnelfm  24182  flimopn  24204  fbflim2  24206  flffbas  24224  fclsnei  24248  flimfnfcls  24257  fclscmp  24259  fcfnei  24264  cnpfcf  24270  alexsubALTlem2  24277  alexsubALTlem3  24278  alexsubALTlem4  24279  alexsubALT  24280  ptcmplem4  24284  qustgplem  24350  tsmsres  24373  tsmsxp  24384  metss  24737  metcnp3  24769  ovoliunnul  25738  ovolicc2lem3  25750  dyadmax  25829  itg2le  25970  bddiblnc  26072  itgcn  26075  ellimc3  26109  lhop1  26244  dvfsumrlim  26261  fta1g  26398  dvply2g  26518  fta1  26541  aalioulem3  26573  aalioulem4  26574  ulmcaulem  26633  ulmcau  26634  logbgcd1irr  27034  xrlimcnp  27208  cxploglim  27217  jensen  27228  lgsqrmodndvds  27592  gausslemma2dlem1a  27604  gausslemma2dlem2  27606  gausslemma2dlem3  27607  lgsquad2lem2  27624  2lgslem1a1  27628  2sqlem6  27662  2sq2  27672  2sqnn  27678  2sqreultblem  27687  nosepdmlem  27922  nodenselem8  27930  eqcuts3  28072  madebdaylemlrcut  28167  addsprop  28244  addsuniflem  28269  negsprop  28303  mulsprop  28398  mulsuniflem  28417  precsex  28486  onsfi  28624  elnnzs  28669  elreno2  28763  brbtwn2  29365  ax5seglem5  29393  axcontlem4  29427  axcontlem10  29433  umgrnloopv  29566  umgrnloop  29568  upgredgpr  29602  numedglnl  29604  usgrausgrb  29632  usgrnloopvALT  29664  usgrnloopALT  29666  usgredg2vlem2  29689  ushgredgedg  29692  ushgredgedgloop  29694  upgrreslem  29767  umgrreslem  29768  nbgr0edglem  29819  nbusgrvtxm1  29842  uvtxnbgrvtx  29856  cusgredg  29887  cusgrres  29911  cusgrsize2inds  29916  cusgrfi  29921  fusgrregdegfi  30032  ewlkle  30068  uspgr2wlkeqi  30110  lfgrwlkprop  30152  lfgrwlknloop  30154  pthdivtx  30194  2pthnloop  30199  upgrwlkdvdelem  30204  upgrspthswlk  30206  usgr2wlkneq  30224  usgr2trlncl  30228  usgr2pthlem  30231  usgr2pth  30232  uspgrn2crct  30279  crctcshwlkn0lem4  30284  crctcshwlkn0lem5  30285  crctcshwlkn0  30292  wlkiswwlks1  30338  wlkiswwlks2  30346  wlkiswwlksupgr2  30348  wwlksnred  30363  wwlksnext  30364  wwlksnextbi  30365  wwlksnextwrd  30368  wwlksnextinj  30370  wwlksnextproplem2  30381  wwlksnextproplem3  30382  wspthsnonn0vne  30388  wspn0  30395  2pthon3v  30414  usgrwwlks2on  30429  umgrwwlks2on  30430  elwspths2on  30433  elwspths2onw  30434  wpthswwlks2on  30435  clwwlk1loop  30461  clwwlkccatlem  30462  umgrclwwlkge2  30464  clwlkclwwlklem2a4  30470  clwlkclwwlklem2a  30471  clwlkclwwlklem3  30474  clwlkclwwlkf1lem3  30479  clwlkclwwlkfo  30482  clwwisshclwwslemlem  30486  erclwwlkeqlen  30492  erclwwlksym  30494  clwwlkf  30520  clwwlknscsh  30535  erclwwlknsym  30543  clwwlknonex2lem2  30581  clwwlknonex2  30582  umgr2cycllem  30628  upgr3v3e3cycl  30663  upgr4cycl4dv4e  30668  eucrctshift  30726  3vfriswmgr  30761  1to2vfriswmgr  30762  1to3vfriswmgr  30763  n4cyclfrgr  30774  4cyclusnfrgr  30775  frgrnbnb  30776  frgrncvvdeqlem8  30789  frgrwopreg  30806  frgr2wwlk1  30812  frgr2wwlkeqm  30814  2clwwlk2clwwlklem  30829  numclwwlk1lem2fo  30841  wlkl0  30850  numclwlk2lem2f  30860  frgrreggt1  30876  frgrreg  30877  frgrregord013  30878  frgrregord13  30879  frgrogt3nreg  30880  eulplig  30969  nmoub3i  31257  ipasslem5  31319  htthlem  31401  ocin  31780  spansneleq  32054  spansnss  32055  elspansn4  32057  h1datomi  32065  nmopub2tALT  32393  nmfnleub2  32410  hstel2  32703  cvnbtwn  32770  spansncv2  32777  dmdmd  32784  dmdbr3  32789  dmdbr4  32790  dmdbr5  32792  mdsl0  32794  mdexchi  32819  cvexchlem  32852  atcv1  32864  atomli  32866  atcvatlem  32869  atcvat2i  32871  chirredi  32878  mdsymlem3  32889  mdsymlem4  32890  sumdmdii  32899  sumdmdlem  32902  cdj1i  32917  ssrelf  33091  f1o3d  33102  fisshasheq  35720  cvxpconn  35824  satfv0  35940  satfsschain  35946  satfrel  35949  satfdm  35951  satfv0fun  35953  sat1el2xp  35961  gonarlem  35976  goalrlem  35978  satffunlem1lem1  35984  satffunlem2lem1  35986  satffunlem2lem2  35988  satffun  35991  mrsubccat  36100  msubvrs  36142  fundmpss  36349  dfon2lem6  36368  dfon2lem8  36370  dfon2lem9  36371  dfon2  36372  wzel  36404  colinearxfr  36658  btwnconn1lem11  36680  lineintmo  36740  in-ax8  36847  ss-ax8  36848  trer  36938  elicc3  36939  finminlem  36940  nn0prpwlem  36944  fnessref  36979  neibastop2  36983  fgmin  36992  tailfb  36999  ordcmp  37069  ee7.2aOLD  37083  dfttc4  37152  bj-ceqsalt0  37630  bj-ceqsalt1  37631  isbasisrelowllem1  38112  isbasisrelowllem2  38113  relowlpssretop  38121  fvineqsneu  38168  fvineqsneq  38169  wl-mo3t  38342  finixpnum  38362  poimirlem26  38398  poimirlem27  38399  poimirlem29  38401  ftc1anc  38453  fdc  38498  heibor1lem  38562  ghomco  38644  rngoueqz  38693  unichnidl  38784  dmncan1  38829  ax12indn  39819  lshpdisj  39863  lub0N  40065  glb0N  40069  leat2  40170  hlrelat2  40279  cvrexchlem  40295  cvratlem  40297  atcvrj0  40304  cvrat2  40305  snatpsubN  40626  linepsubN  40628  pmaple  40637  pmapsub  40644  elpaddn0  40676  paddasslem5  40700  trlval2  41039  cdlemn11pre  42086  dihord2pre  42101  mapdordlem2  42513  sn-sup2  43382  fsuppind  43439  pell1qrgap  43718  dford3lem1  43870  hbtlem5  43972  onexlimgt  44087  onsucf1olem  44114  omcl2  44177  tfsconcat0b  44190  ntrneiiso  44934  sbiota1  45261  19.41rg  45376  ee223  45460  or2expropbilem1  47923  funressnfv  47934  fcoresf1  47960  2reuimp  48006  f1oresf1o2  48182  zm1nn  48193  nltle2tri  48204  el1fzopredsuc  48217  modlt0b  48260  mod2addne  48261  muldvdsfacgt  48277  muldvdsfacm1  48278  elsetpreimafvssdm  48289  imasetpreimafvbijlemf1  48307  iccpartlt  48327  iccpartgt  48330  iccelpart  48336  icceuelpart  48339  iccpartnel  48341  fargshiftfo  48345  fargshiftfva  48346  lswn0  48347  ich2exprop  48374  prsprel  48390  sprsymrelfolem2  48396  sprsymrelfo  48400  poprelb  48427  reuopreuprim  48429  goldbachthlem2  48452  odz2prm2pw  48469  fmtnoprmfac1  48471  fmtnofac2lem  48474  prmdvdsfmtnof1lem2  48491  2pwp1prm  48495  sfprmdvdsmersenne  48509  lighneallem3  48513  requad01  48540  requad2  48542  even3prm2  48638  fppr2odd  48650  fpprwpprb  48659  gbegt5  48680  sbgoldbwt  48696  sbgoldbalt  48700  sbgoldbm  48703  bgoldbtbndlem2  48725  bgoldbtbndlem3  48726  bgoldbtbndlem4  48727  bgoldbtbnd  48728  tgblthelfgott  48734  tgoldbach  48736  isubgredg  48785  grimuhgr  48806  grimcnv  48807  grimco  48808  isuspgrim0  48813  isuspgrimlem  48814  uhgrimisgrgriclem  48849  clnbgrgrimlem  48852  grimedg  48854  grtriprop  48860  cycl3grtri  48866  grimgrtri  48868  isubgr3stgrlem6  48890  uspgrlimlem3  48909  uspgrlimlem4  48910  grlimgrtrilem2  48921  grlicsym  48932  clnbgr3stgrgrlim  48938  clnbgr3stgrgrlic  48939  gpgedg2ov  48985  gpgedg2iv  48986  pgnbgreunbgrlem3  49037  pgnbgreunbgrlem6  49043  upgrwlkupwlk  49059  lmod0rng  49147  idomcanl  49265  ztprmneprm  49280  ply1mulgsumlem1  49319  ply1mulgsumlem2  49320  lcoel0  49361  linindslinci  49381  lindslinindimp2lem4  49394  lindslinindsimp2lem5  49395  snlindsntor  49404  ldepspr  49406  lincresunit2  49411  fllog2  49501  dignn0ldlem  49535  dignn0flhalflem1  49548  nn0sumshdiglemA  49552  nn0sumshdiglemB  49553  itcovalt2  49610  resum2sqorgt0  49642  eenglngeehlnmlem2  49671  rrx2linest  49675  itscnhlc0xyqsol  49698  itsclc0  49704  setrec1lem2  50617  aacllem  50775