Theorem com23 86

Description: Commutation of antecedents. Swap 2nd and 3rd. Deduction associated with com12 32. (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 42	. 2 ⊢ (𝜒 → ((𝜒 → 𝜃) → 𝜃))
3	1, 2	syl9 77	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  87  com13  88  pm2.04  90  pm2.86d  108  impcomd  411  expcomd  416  impancom  451  a2and  845  dedlem0b  1044  sbequ1  2249  moexexlem  2619  ralrimdvva  3184  ceqsal1t  3469  ceqsalt  3470  spcimgft  3501  vtoclgft  3507  elabgtOLD  3628  sbciegftOLD  3780  reupick  4280  reusv3  5344  sbcop1  5431  propeqop  5450  pwssun  5511  wefrc  5613  ssrel  5726  ssrel2  5728  ssrelrel  5739  ssrelrn  5837  tz7.7  6333  ordtr2  6352  onmindif  6401  unizlim  6431  funssres  6526  f1ssf1  6796  fvmptt  6950  fveqdmss  7012  fvcofneq  7027  funsndifnop  7085  funfvima2  7167  isoini  7275  isopolem  7282  weniso  7291  f1ocnv2d  7602  limsssuc  7783  tfindsg  7794  limomss  7804  findsg  7830  funcnvuni  7865  f1oweALT  7907  funelss  7982  bropopvvv  8023  bropfvvvvlem  8024  bropfvvvv  8025  f1o2ndf1  8055  frxp  8059  soseq  8092  suppfnss  8122  onfununi  8264  tz7.49  8367  omordi  8484  omlimcl  8496  omass  8498  oeordsuc  8512  nnmordi  8549  nnmord  8550  omabs  8569  xpdom2  8989  infensuc  9072  findcard2  9078  findcard2d  9080  findcard3  9172  frfi  9174  fsuppres  9283  dffi2  9313  elfiun  9320  ordiso2  9407  ordtypelem7  9416  suc11reg  9515  inf3lem2  9525  noinfep  9556  cantnfle  9567  cantnflem1  9585  cantnf  9589  ttrclss  9616  trcl  9624  epfrs  9627  frr3g  9652  r1sdom  9670  updjud  9830  dfac8alem  9923  indcardi  9935  alephordi  9968  dfac12lem3  10040  pwsdompw  10097  cofsmo  10163  cfcoflem  10166  coftr  10167  isf32lem2  10248  isf32lem9  10255  axcc3  10332  domtriomlem  10336  axdc3lem2  10345  axdc3lem4  10347  zorn2lem4  10393  zorn2lem6  10395  zorn2lem7  10396  ttukeylem6  10408  uniimadom  10438  konigthlem  10462  fpwwe2lem7  10531  tskord  10674  tskcard  10675  grupr  10691  gruiin  10704  grudomon  10711  grur1a  10713  genpn0  10897  genpcd  10900  distrlem5pr  10921  psslinpr  10925  ltaddpr  10928  ltexprlem3  10932  ltexprlem6  10935  ltapr  10939  prlem936  10941  suplem1pr  10946  axpre-sup  11063  1re  11115  dedekindle  11280  lemul12a  11982  divgt0  11993  divge0  11994  lbreu  12075  sup2  12081  bndndx  12383  elnnz  12481  nzadd  12523  fzind  12574  fnn0ind  12575  uzwo  12812  lbzbi  12837  zmax  12846  zbtwnre  12847  irradd  12874  irrmul  12875  ledivge1le  12966  xrub  13214  supxrunb2  13222  infmremnf  13246  iccid  13293  uzsubsubfz  13449  fzrevral  13515  elfz0fzfz0  13536  fz0fzelfz0  13537  elfzmlbp  13542  elincfzoext  13626  ssfzoulel  13663  ssfzo12bi  13664  fzoopth  13665  elfzonelfzo  13672  elfznelfzo  13675  elfznelfzob  13676  injresinjlem  13690  fleqceilz  13758  modaddmodup  13841  uzindi  13889  suppssfz  13901  mptnn0fsuppr  13906  le2sq2  14042  sqlecan  14116  facdiv  14194  facwordi  14196  faclbnd  14197  hashimarni  14348  hash2prd  14382  hashle2pr  14384  pr2pwpr  14386  fundmge2nop0  14409  fi1uzind  14414  brfi1indALT  14417  swrdnd2  14562  swrdnnn0nd  14563  swrdnd0  14564  pfxnd0  14595  swrdswrdlem  14610  swrdswrd  14611  ccatopth2  14623  wrd2ind  14629  pfxccatin12lem2a  14633  swrdccatin2  14635  pfxccatin12lem2  14637  pfxccatin12lem3  14638  swrdccat  14641  swrdccat3blem  14645  reuccatpfxs1lem  14652  repswswrd  14690  cshwidxmod  14709  cshwidx0  14712  2cshwcshw  14732  cshwcsh2id  14735  cau3lem  15262  caubnd  15266  climrlim2  15454  rlimcn3  15497  mulcn2  15503  climcau  15578  climbdd  15579  caucvg  15586  modfsummod  15701  p1modz1  16170  dvdsle  16221  dvdsdivcl  16227  ltoddhalfle  16272  halfleoddlt  16273  ndvdssub  16320  gcdcllem1  16410  dvdslegcd  16415  bezoutlem4  16453  dfgcd2  16457  lcmf  16544  lcmfunsnlem1  16548  lcmfunsnlem2lem1  16549  lcmfunsnlem  16552  lcmfdvdsb  16554  lcmfun  16556  coprmdvds1  16563  divgcdcoprm0  16576  cncongr1  16578  cncongr2  16579  prmfac1  16631  pcqcl  16768  dvdsprmpweqle  16798  oddprmdvds  16815  prmpwdvds  16816  infpnlem1  16822  prmgaplem5  16967  prmgaplem6  16968  prmgaplem7  16969  cshwshashlem1  17007  cictr  17712  initoeu2lem1  17921  initoeu2  17923  clatleglb  18424  lidrididd  18544  mulgaddcom  18977  mulginvcom  18978  cycsubm  19081  cyccom  19082  gsmsymgreqlem2  19310  symggen  19349  psgnunilem4  19376  sylow2blem3  19501  frgpnabllem1  19752  imasabl  19755  dprddisj2  19920  lmodfopnelem1  20801  lssssr  20857  lss1d  20866  lspsncv0  21053  rnglidlmcl  21123  rngqiprngimfo  21208  nzerooringczr  21387  pzriprnglem5  21392  pzriprnglem8  21395  znrrg  21472  mplcoe5lem  21944  cply1mul  22181  coe1fzgsumdlem  22188  gsummoncoe1  22193  evl1gsumdlem  22241  mamufacex  22281  dmatelnd  22381  scmataddcl  22401  scmatsubcl  22402  scmatmulcl  22403  smatvscl  22409  mavmulsolcl  22436  mdetdiagid  22485  cramerlem3  22574  pmatcoe1fsupp  22586  cpmatacl  22601  cpmatmcllem  22603  mp2pm2mplem4  22694  chpscmat  22727  chfacfisf  22739  chfacfisfcpmat  22740  uniopn  22782  opnnei  23005  neindisj2  23008  restcls  23066  restntr  23067  tgcnp  23138  subbascn  23139  iscnp4  23148  lpcls  23249  cmpsublem  23284  cmpsub  23285  tgcmp  23286  cmpcld  23287  dfconn2  23304  1stcrest  23338  2ndcdisj  23341  1stccnp  23347  comppfsc  23417  kgencn2  23442  txlm  23533  kqreglem1  23626  filin  23739  isfil2  23741  ufilmax  23792  ufileu  23804  filufint  23805  cfinufil  23813  elfm2  23833  rnelfmlem  23837  rnelfm  23838  flimopn  23860  fbflim2  23862  flffbas  23880  fclsnei  23904  flimfnfcls  23913  fclscmp  23915  fcfnei  23920  cnpfcf  23926  alexsubALTlem2  23933  alexsubALTlem3  23934  alexsubALTlem4  23935  alexsubALT  23936  ptcmplem4  23940  qustgplem  24006  tsmsres  24029  tsmsxp  24040  metss  24394  metcnp3  24426  ovoliunnul  25406  ovolicc2lem3  25418  dyadmax  25497  itg2le  25638  bddiblnc  25741  itgcn  25744  ellimc3  25778  lhop1  25917  dvfsumrlim  25936  fta1g  26073  dvply2g  26190  fta1  26214  aalioulem3  26240  aalioulem4  26241  ulmcaulem  26301  ulmcau  26302  logbgcd1irr  26702  xrlimcnp  26876  cxploglim  26886  jensen  26897  lgsqrmodndvds  27262  gausslemma2dlem1a  27274  gausslemma2dlem2  27276  gausslemma2dlem3  27277  lgsquad2lem2  27294  2lgslem1a1  27298  2sqlem6  27332  2sq2  27342  2sqnn  27348  2sqreultblem  27357  nosepdmlem  27593  nodenselem8  27601  eqscut3  27735  madebdaylemlrcut  27813  addsprop  27888  addsuniflem  27913  negsprop  27946  mulsprop  28038  mulsuniflem  28057  precsex  28125  onsfi  28252  elnnzs  28294  brbtwn2  28850  ax5seglem5  28878  axcontlem4  28912  axcontlem10  28918  umgrnloopv  29051  umgrnloop  29053  upgredgpr  29087  numedglnl  29089  usgrausgrb  29114  usgrnloopvALT  29146  usgrnloopALT  29148  usgredg2vlem2  29171  ushgredgedg  29174  ushgredgedgloop  29176  upgrreslem  29249  umgrreslem  29250  nbgr0edglem  29301  nbusgrvtxm1  29324  uvtxnbgrvtx  29338  cusgredg  29369  cusgrres  29394  cusgrsize2inds  29399  cusgrfi  29404  fusgrregdegfi  29515  ewlkle  29551  uspgr2wlkeqi  29593  lfgrwlkprop  29631  lfgrwlknloop  29633  pthdivtx  29672  2pthnloop  29676  upgrwlkdvdelem  29681  upgrspthswlk  29683  usgr2wlkneq  29701  usgr2trlncl  29705  usgr2pthlem  29708  usgr2pth  29709  uspgrn2crct  29753  crctcshwlkn0lem4  29758  crctcshwlkn0lem5  29759  crctcshwlkn0  29766  wlkiswwlks1  29812  wlkiswwlks2  29820  wlkiswwlksupgr2  29822  wwlksnred  29837  wwlksnext  29838  wwlksnextbi  29839  wwlksnextwrd  29842  wwlksnextinj  29844  wwlksnextproplem2  29855  wwlksnextproplem3  29856  wspthsnonn0vne  29862  wspn0  29869  2pthon3v  29888  umgrwwlks2on  29902  elwspths2on  29905  wpthswwlks2on  29906  clwwlk1loop  29932  clwwlkccatlem  29933  umgrclwwlkge2  29935  clwlkclwwlklem2a4  29941  clwlkclwwlklem2a  29942  clwlkclwwlklem3  29945  clwlkclwwlkf1lem3  29950  clwlkclwwlkfo  29953  clwwisshclwwslemlem  29957  erclwwlkeqlen  29963  erclwwlksym  29965  clwwlkf  29991  clwwlknscsh  30006  erclwwlknsym  30014  clwwlknonex2lem2  30052  clwwlknonex2  30053  upgr3v3e3cycl  30124  upgr4cycl4dv4e  30129  eucrctshift  30187  3vfriswmgr  30222  1to2vfriswmgr  30223  1to3vfriswmgr  30224  n4cyclfrgr  30235  4cyclusnfrgr  30236  frgrnbnb  30237  frgrncvvdeqlem8  30250  frgrwopreg  30267  frgr2wwlk1  30273  frgr2wwlkeqm  30275  2clwwlk2clwwlklem  30290  numclwwlk1lem2fo  30302  wlkl0  30311  numclwlk2lem2f  30321  frgrreggt1  30337  frgrreg  30338  frgrregord013  30339  frgrregord13  30340  frgrogt3nreg  30341  eulplig  30429  nmoub3i  30717  ipasslem5  30779  htthlem  30861  ocin  31240  spansneleq  31514  spansnss  31515  elspansn4  31517  h1datomi  31525  nmopub2tALT  31853  nmfnleub2  31870  hstel2  32163  cvnbtwn  32230  spansncv2  32237  dmdmd  32244  dmdbr3  32249  dmdbr4  32250  dmdbr5  32252  mdsl0  32254  mdexchi  32279  cvexchlem  32312  atcv1  32324  atomli  32326  atcvatlem  32329  atcvat2i  32331  chirredi  32338  mdsymlem3  32349  mdsymlem4  32350  sumdmdii  32359  sumdmdlem  32362  cdj1i  32377  ssrelf  32560  f1o3d  32570  fisshasheq  35098  umgr2cycllem  35123  cvxpconn  35225  satfv0  35341  satfsschain  35347  satfrel  35350  satfdm  35352  satfv0fun  35354  sat1el2xp  35362  gonarlem  35377  goalrlem  35379  satffunlem1lem1  35385  satffunlem2lem1  35387  satffunlem2lem2  35389  satffun  35392  mrsubccat  35501  msubvrs  35543  fundmpss  35750  dfon2lem6  35772  dfon2lem8  35774  dfon2lem9  35775  dfon2  35776  wzel  35808  colinearxfr  36059  btwnconn1lem11  36081  lineintmo  36141  in-ax8  36208  ss-ax8  36209  trer  36300  elicc3  36301  finminlem  36302  nn0prpwlem  36306  fnessref  36341  neibastop2  36345  fgmin  36354  tailfb  36361  ordcmp  36431  ee7.2aOLD  36445  bj-cbvalimt  36623  bj-ceqsalt0  36868  bj-ceqsalt1  36869  isbasisrelowllem1  37339  isbasisrelowllem2  37340  relowlpssretop  37348  fvineqsneu  37395  fvineqsneq  37396  wl-mo3t  37560  finixpnum  37595  matunitlindflem1  37606  matunitlindflem2  37607  poimirlem26  37636  poimirlem27  37637  poimirlem29  37639  ftc1anc  37691  fdc  37735  heibor1lem  37799  ghomco  37881  rngoueqz  37930  unichnidl  38021  dmncan1  38066  ax12indn  38932  lshpdisj  38976  lub0N  39178  glb0N  39182  leat2  39283  hlrelat2  39392  cvrexchlem  39408  cvratlem  39410  atcvrj0  39417  cvrat2  39418  snatpsubN  39739  linepsubN  39741  pmaple  39750  pmapsub  39757  elpaddn0  39789  paddasslem5  39813  trlval2  40152  cdlemn11pre  41199  dihord2pre  41214  mapdordlem2  41626  sn-sup2  42474  fsuppind  42573  pell1qrgap  42857  dford3lem1  43009  hbtlem5  43111  onexlimgt  43226  onsucf1olem  43253  omcl2  43316  tfsconcat0b  43329  ntrneiiso  44074  sbiota1  44417  19.41rg  44534  ee223  44618  or2expropbilem1  47026  funressnfv  47037  fcoresf1  47063  2reuimp  47109  f1oresf1o2  47285  zm1nn  47296  nltle2tri  47307  el1fzopredsuc  47319  modlt0b  47357  mod2addne  47358  elsetpreimafvssdm  47380  imasetpreimafvbijlemf1  47398  iccpartlt  47418  iccpartgt  47421  iccelpart  47427  icceuelpart  47430  iccpartnel  47432  fargshiftfo  47436  fargshiftfva  47437  lswn0  47438  ich2exprop  47465  prsprel  47481  sprsymrelfolem2  47487  sprsymrelfo  47491  poprelb  47518  reuopreuprim  47520  goldbachthlem2  47540  odz2prm2pw  47557  fmtnoprmfac1  47559  fmtnofac2lem  47562  prmdvdsfmtnof1lem2  47579  2pwp1prm  47583  sfprmdvdsmersenne  47597  lighneallem3  47601  requad01  47615  requad2  47617  even3prm2  47713  fppr2odd  47725  fpprwpprb  47734  gbegt5  47755  sbgoldbwt  47771  sbgoldbalt  47775  sbgoldbm  47778  bgoldbtbndlem2  47800  bgoldbtbndlem3  47801  bgoldbtbndlem4  47802  bgoldbtbnd  47803  tgblthelfgott  47809  tgoldbach  47811  isubgredg  47860  grimuhgr  47881  grimcnv  47882  grimco  47883  isuspgrim0  47888  isuspgrimlem  47889  uhgrimisgrgriclem  47924  clnbgrgrimlem  47927  grimedg  47929  grtriprop  47935  cycl3grtri  47941  grimgrtri  47943  isubgr3stgrlem6  47965  uspgrlimlem3  47984  uspgrlimlem4  47985  grlimgrtrilem2  47996  grlicsym  48007  clnbgr3stgrgrlim  48013  clnbgr3stgrgrlic  48014  gpgedg2ov  48060  gpgedg2iv  48061  pgnbgreunbgrlem3  48112  pgnbgreunbgrlem6  48118  upgrwlkupwlk  48134  lmod0rng  48223  ztprmneprm  48341  ply1mulgsumlem1  48381  ply1mulgsumlem2  48382  lcoel0  48423  linindslinci  48443  lindslinindimp2lem4  48456  lindslinindsimp2lem5  48457  snlindsntor  48466  ldepspr  48468  lincresunit2  48473  fllog2  48563  dignn0ldlem  48597  dignn0flhalflem1  48610  nn0sumshdiglemA  48614  nn0sumshdiglemB  48615  itcovalt2  48672  resum2sqorgt0  48704  eenglngeehlnmlem2  48733  rrx2linest  48737  itscnhlc0xyqsol  48760  itsclc0  48766  setrec1lem2  49683  aacllem  49796