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

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  88  com13  89  pm2.04  91  pm2.86d  109  impcomd  416  expcomd  421  impancom  456  a2and  858  dedlem0b  1058  sbequ1  2290  moexexlem  2660  ralrimdvva  3226  ceqsal1t  3495  ceqsalt  3496  spcimgft  3523  vtoclgft  3529  elabgtOLD  3641  reupick  4290  reusv3  5374  sbcop1  5468  propeqop  5488  pwssun  5551  wefrc  5653  ssrel  5767  ssrel2  5769  ssrelrel  5780  ssrelrn  5882  tz7.7  6384  ordtr2  6404  onmindif  6453  unizlim  6483  funssres  6578  f1ssf1  6851  fvmptt  7008  fveqdmss  7071  fvcofneq  7086  funsndifnop  7146  funfvima2  7227  isoini  7334  isopolem  7341  weniso  7350  f1ocnv2d  7661  limsssuc  7842  tfindsg  7853  limomss  7863  findsg  7890  funcnvuni  7925  f1oweALT  7965  funelss  8040  bropopvvv  8081  bropfvvvvlem  8082  bropfvvvv  8083  f1o2ndf1  8113  frxp  8118  soseq  8151  suppfnss  8181  onfununi  8324  tz7.49  8428  omordi  8547  omlimcl  8559  omass  8561  oeordsuc  8576  nnmordi  8613  nnmord  8614  omabs  8633  xpdom2  9056  infensuc  9139  findcard2  9145  findcard2d  9147  findcard3  9239  frfi  9241  fsuppres  9349  dffi2  9379  elfiun  9386  ordiso2  9473  ordtypelem7  9482  suc11reg  9584  inf3lem2  9594  noinfep  9625  cantnfle  9636  cantnflem1  9654  cantnf  9658  ttrclss  9685  trcl  9693  epfrs  9696  frr3g  9724  r1sdom  9742  updjud  9916  dfac8alem  10009  indcardi  10021  alephordi  10054  dfac12lem3  10125  pwsdompw  10182  cofsmo  10249  cfcoflem  10252  coftr  10253  isf32lem2  10334  isf32lem9  10341  axcc3  10418  domtriomlem  10422  axdc3lem2  10431  axdc3lem4  10433  zorn2lem4  10479  zorn2lem6  10481  zorn2lem7  10482  ttukeylem6  10494  uniimadom  10524  konigthlem  10549  fpwwe2lem7  10618  tskord  10761  tskcard  10762  grupr  10778  gruiin  10791  grudomon  10798  grur1a  10800  genpn0  10984  genpcd  10987  distrlem5pr  11008  psslinpr  11012  ltaddpr  11015  ltexprlem3  11019  ltexprlem6  11022  ltapr  11026  prlem936  11028  suplem1pr  11033  axpre-sup  11150  1re  11204  dedekindle  11370  lemul12a  12069  divgt0  12079  divge0  12080  lbreu  12161  sup2  12167  bndndx  12499  elnnz  12597  nzadd  12638  fzind  12690  fnn0ind  12691  uzwo  12931  lbzbi  12956  zmax  12965  zbtwnre  12966  irradd  12993  irrmul  12994  ledivge1le  13085  xrub  13334  supxrunb2  13342  infmremnf  13366  iccid  13413  uzsubsubfz  13570  fzrevral  13636  elfz0fzfz0  13657  fz0fzelfz0  13658  elfzmlbp  13663  elincfzoext  13748  ssfzoulel  13785  ssfzo12bi  13786  fzoopth  13787  elfzonelfzo  13794  elfznelfzo  13798  elfznelfzob  13799  injresinjlem  13815  fleqceilz  13883  modaddmodup  13966  uzindi  14014  suppssfz  14026  mptnn0fsuppr  14031  le2sq2  14167  sqlecan  14241  facdiv  14319  facwordi  14321  faclbnd  14322  hashimarni  14474  hash2prd  14508  hashle2pr  14510  pr2pwpr  14512  fundmge2nop0  14535  fi1uzind  14540  brfi1indALT  14543  swrdnd2  14689  swrdnnn0nd  14690  swrdnd0  14691  pfxnd0  14722  swrdswrdlem  14737  swrdswrd  14738  ccatopth2  14750  wrd2ind  14756  pfxccatin12lem2a  14760  swrdccatin2  14762  pfxccatin12lem2  14764  pfxccatin12lem3  14765  swrdccat  14768  swrdccat3blem  14772  reuccatpfxs1lem  14779  repswswrd  14817  cshwidxmod  14836  cshwidx0  14839  2cshwcshw  14858  cshwcsh2id  14861  cau3lem  15402  caubnd  15406  climrlim2  15594  rlimcn3  15637  mulcn2  15643  climcau  15718  climbdd  15719  caucvg  15726  modfsummod  15842  p1modz1  16313  dvdsle  16364  dvdsdivcl  16370  ltoddhalfle  16415  halfleoddlt  16416  ndvdssub  16463  gcdcllem1  16553  dvdslegcd  16558  bezoutlem4  16596  dfgcd2  16600  lcmf  16687  lcmfunsnlem1  16691  lcmfunsnlem2lem1  16692  lcmfunsnlem  16695  lcmfdvdsb  16697  lcmfun  16699  coprmdvds1  16706  divgcdcoprm0  16719  cncongr1  16721  cncongr2  16722  prmfac1  16775  pcqcl  16912  dvdsprmpweqle  16942  oddprmdvds  16959  prmpwdvds  16960  infpnlem1  16966  prmgaplem5  17111  prmgaplem6  17112  prmgaplem7  17113  cshwshashlem1  17151  cictr  17858  initoeu2lem1  18067  initoeu2  18069  clatleglb  18570  lidrididd  18724  mulgaddcom  19160  mulginvcom  19161  cycsubm  19269  cyccom  19270  gsmsymgreqlem2  19497  symggen  19536  psgnunilem4  19563  sylow2blem3  19688  frgpnabllem1  19939  imasabl  19942  dprddisj2  20107  lmodfopnelem1  20993  lssssr  21049  lss1d  21058  lspsncv0  21244  rnglidlmcl  21315  lidlunin0  21335  unichnlidl  21336  rngqiprngimfo  21408  nzerooringczr  21595  pzriprnglem5  21600  pzriprnglem8  21603  znrrg  21680  mplcoe5lem  22155  cply1mul  22421  coe1fzgsumdlem  22428  gsummoncoe1  22433  evl1gsumdlem  22481  mamufacex  22518  dmatelnd  22618  scmataddcl  22638  scmatsubcl  22639  scmatmulcl  22640  smatvscl  22646  mavmulsolcl  22673  mdetdiagid  22722  cramerlem3  22811  pmatcoe1fsupp  22823  cpmatacl  22838  cpmatmcllem  22840  mp2pm2mplem4  22931  chpscmat  22964  chfacfisf  22976  chfacfisfcpmat  22977  uniopn  23019  opnnei  23242  neindisj2  23245  restcls  23303  restntr  23304  tgcnp  23375  subbascn  23376  iscnp4  23385  lpcls  23486  cmpsublem  23521  cmpsub  23522  tgcmp  23523  cmpcld  23524  dfconn2  23541  1stcrest  23575  2ndcdisj  23578  1stccnp  23584  comppfsc  23654  kgencn2  23679  txlm  23770  kqreglem1  23863  filin  23976  isfil2  23978  ufilmax  24029  ufileu  24041  filufint  24042  cfinufil  24050  elfm2  24070  rnelfmlem  24074  rnelfm  24075  flimopn  24097  fbflim2  24099  flffbas  24117  fclsnei  24141  flimfnfcls  24150  fclscmp  24152  fcfnei  24157  cnpfcf  24163  alexsubALTlem2  24170  alexsubALTlem3  24171  alexsubALTlem4  24172  alexsubALT  24173  ptcmplem4  24177  qustgplem  24243  tsmsres  24266  tsmsxp  24277  metss  24630  metcnp3  24662  ovoliunnul  25631  ovolicc2lem3  25643  dyadmax  25722  itg2le  25863  bddiblnc  25966  itgcn  25969  ellimc3  26003  lhop1  26138  dvfsumrlim  26155  fta1g  26292  dvply2g  26411  fta1  26434  aalioulem3  26460  aalioulem4  26461  ulmcaulem  26519  ulmcau  26520  logbgcd1irr  26921  xrlimcnp  27095  cxploglim  27104  jensen  27115  lgsqrmodndvds  27479  gausslemma2dlem1a  27491  gausslemma2dlem2  27493  gausslemma2dlem3  27494  lgsquad2lem2  27511  2lgslem1a1  27515  2sqlem6  27549  2sq2  27559  2sqnn  27565  2sqreultblem  27574  nosepdmlem  27809  nodenselem8  27817  eqcuts3  27959  madebdaylemlrcut  28054  addsprop  28131  addsuniflem  28156  negsprop  28190  mulsprop  28285  mulsuniflem  28304  precsex  28373  onsfi  28511  elnnzs  28556  elreno2  28650  brbtwn2  29192  ax5seglem5  29220  axcontlem4  29254  axcontlem10  29260  umgrnloopv  29393  umgrnloop  29395  upgredgpr  29429  numedglnl  29431  usgrausgrb  29456  usgrnloopvALT  29488  usgrnloopALT  29490  usgredg2vlem2  29513  ushgredgedg  29516  ushgredgedgloop  29518  upgrreslem  29591  umgrreslem  29592  nbgr0edglem  29643  nbusgrvtxm1  29666  uvtxnbgrvtx  29680  cusgredg  29711  cusgrres  29735  cusgrsize2inds  29740  cusgrfi  29745  fusgrregdegfi  29856  ewlkle  29892  uspgr2wlkeqi  29934  lfgrwlkprop  29972  lfgrwlknloop  29974  pthdivtx  30013  2pthnloop  30017  upgrwlkdvdelem  30022  upgrspthswlk  30024  usgr2wlkneq  30042  usgr2trlncl  30046  usgr2pthlem  30049  usgr2pth  30050  uspgrn2crct  30094  crctcshwlkn0lem4  30099  crctcshwlkn0lem5  30100  crctcshwlkn0  30107  wlkiswwlks1  30153  wlkiswwlks2  30161  wlkiswwlksupgr2  30163  wwlksnred  30178  wwlksnext  30179  wwlksnextbi  30180  wwlksnextwrd  30183  wwlksnextinj  30185  wwlksnextproplem2  30196  wwlksnextproplem3  30197  wspthsnonn0vne  30203  wspn0  30210  2pthon3v  30229  usgrwwlks2on  30244  umgrwwlks2on  30245  elwspths2on  30248  elwspths2onw  30249  wpthswwlks2on  30250  clwwlk1loop  30276  clwwlkccatlem  30277  umgrclwwlkge2  30279  clwlkclwwlklem2a4  30285  clwlkclwwlklem2a  30286  clwlkclwwlklem3  30289  clwlkclwwlkf1lem3  30294  clwlkclwwlkfo  30297  clwwisshclwwslemlem  30301  erclwwlkeqlen  30307  erclwwlksym  30309  clwwlkf  30335  clwwlknscsh  30350  erclwwlknsym  30358  clwwlknonex2lem2  30396  clwwlknonex2  30397  upgr3v3e3cycl  30468  upgr4cycl4dv4e  30473  eucrctshift  30531  3vfriswmgr  30566  1to2vfriswmgr  30567  1to3vfriswmgr  30568  n4cyclfrgr  30579  4cyclusnfrgr  30580  frgrnbnb  30581  frgrncvvdeqlem8  30594  frgrwopreg  30611  frgr2wwlk1  30617  frgr2wwlkeqm  30619  2clwwlk2clwwlklem  30634  numclwwlk1lem2fo  30646  wlkl0  30655  numclwlk2lem2f  30665  frgrreggt1  30681  frgrreg  30682  frgrregord013  30683  frgrregord13  30684  frgrogt3nreg  30685  eulplig  30774  nmoub3i  31062  ipasslem5  31124  htthlem  31206  ocin  31585  spansneleq  31859  spansnss  31860  elspansn4  31862  h1datomi  31870  nmopub2tALT  32198  nmfnleub2  32215  hstel2  32508  cvnbtwn  32575  spansncv2  32582  dmdmd  32589  dmdbr3  32594  dmdbr4  32595  dmdbr5  32597  mdsl0  32599  mdexchi  32624  cvexchlem  32657  atcv1  32669  atomli  32671  atcvatlem  32674  atcvat2i  32676  chirredi  32683  mdsymlem3  32694  mdsymlem4  32695  sumdmdii  32704  sumdmdlem  32707  cdj1i  32722  ssrelf  32897  f1o3d  32908  fisshasheq  35501  umgr2cycllem  35527  cvxpconn  35629  satfv0  35745  satfsschain  35751  satfrel  35754  satfdm  35756  satfv0fun  35758  sat1el2xp  35766  gonarlem  35781  goalrlem  35783  satffunlem1lem1  35789  satffunlem2lem1  35791  satffunlem2lem2  35793  satffun  35796  mrsubccat  35905  msubvrs  35947  fundmpss  36154  dfon2lem6  36173  dfon2lem8  36175  dfon2lem9  36176  dfon2  36177  wzel  36209  colinearxfr  36462  btwnconn1lem11  36484  lineintmo  36544  in-ax8  36621  ss-ax8  36622  trer  36712  elicc3  36713  finminlem  36714  nn0prpwlem  36718  fnessref  36753  neibastop2  36757  fgmin  36766  tailfb  36773  ordcmp  36843  ee7.2aOLD  36857  dfttc4  36926  bj-ceqsalt0  37404  bj-ceqsalt1  37405  isbasisrelowllem1  37884  isbasisrelowllem2  37885  relowlpssretop  37893  fvineqsneu  37940  fvineqsneq  37941  wl-mo3t  38114  finixpnum  38139  matunitlindflem1  38150  matunitlindflem2  38151  poimirlem26  38180  poimirlem27  38181  poimirlem29  38183  ftc1anc  38235  fdc  38279  heibor1lem  38343  ghomco  38425  rngoueqz  38474  unichnidl  38565  dmncan1  38610  ax12indn  39602  lshpdisj  39646  lub0N  39848  glb0N  39852  leat2  39953  hlrelat2  40062  cvrexchlem  40078  cvratlem  40080  atcvrj0  40087  cvrat2  40088  snatpsubN  40409  linepsubN  40411  pmaple  40420  pmapsub  40427  elpaddn0  40459  paddasslem5  40483  trlval2  40822  cdlemn11pre  41869  dihord2pre  41884  mapdordlem2  42296  sn-sup2  43150  fsuppind  43209  pell1qrgap  43488  dford3lem1  43640  hbtlem5  43742  onexlimgt  43857  onsucf1olem  43884  omcl2  43947  tfsconcat0b  43960  ntrneiiso  44704  sbiota1  45031  19.41rg  45146  ee223  45230  or2expropbilem1  47653  funressnfv  47664  fcoresf1  47690  2reuimp  47736  f1oresf1o2  47912  zm1nn  47923  nltle2tri  47934  el1fzopredsuc  47947  modlt0b  47990  mod2addne  47991  muldvdsfacgt  48007  muldvdsfacm1  48008  elsetpreimafvssdm  48019  imasetpreimafvbijlemf1  48037  iccpartlt  48057  iccpartgt  48060  iccelpart  48066  icceuelpart  48069  iccpartnel  48071  fargshiftfo  48075  fargshiftfva  48076  lswn0  48077  ich2exprop  48104  prsprel  48120  sprsymrelfolem2  48126  sprsymrelfo  48130  poprelb  48157  reuopreuprim  48159  goldbachthlem2  48182  odz2prm2pw  48199  fmtnoprmfac1  48201  fmtnofac2lem  48204  prmdvdsfmtnof1lem2  48221  2pwp1prm  48225  sfprmdvdsmersenne  48239  lighneallem3  48243  requad01  48270  requad2  48272  even3prm2  48368  fppr2odd  48380  fpprwpprb  48389  gbegt5  48410  sbgoldbwt  48426  sbgoldbalt  48430  sbgoldbm  48433  bgoldbtbndlem2  48455  bgoldbtbndlem3  48456  bgoldbtbndlem4  48457  bgoldbtbnd  48458  tgblthelfgott  48464  tgoldbach  48466  isubgredg  48515  grimuhgr  48536  grimcnv  48537  grimco  48538  isuspgrim0  48543  isuspgrimlem  48544  uhgrimisgrgriclem  48579  clnbgrgrimlem  48582  grimedg  48584  grtriprop  48590  cycl3grtri  48596  grimgrtri  48598  isubgr3stgrlem6  48620  uspgrlimlem3  48639  uspgrlimlem4  48640  grlimgrtrilem2  48651  grlicsym  48662  clnbgr3stgrgrlim  48668  clnbgr3stgrgrlic  48669  gpgedg2ov  48715  gpgedg2iv  48716  pgnbgreunbgrlem3  48767  pgnbgreunbgrlem6  48773  upgrwlkupwlk  48789  lmod0rng  48878  ztprmneprm  49007  ply1mulgsumlem1  49046  ply1mulgsumlem2  49047  lcoel0  49088  linindslinci  49108  lindslinindimp2lem4  49121  lindslinindsimp2lem5  49122  snlindsntor  49131  ldepspr  49133  lincresunit2  49138  fllog2  49228  dignn0ldlem  49262  dignn0flhalflem1  49275  nn0sumshdiglemA  49279  nn0sumshdiglemB  49280  itcovalt2  49337  resum2sqorgt0  49369  eenglngeehlnmlem2  49398  rrx2linest  49402  itscnhlc0xyqsol  49425  itsclc0  49431  setrec1lem2  50346  aacllem  50470