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  2284  moexexlem  2652  ralrimdvva  3218  ceqsal1t  3483  ceqsalt  3484  spcimgft  3511  vtoclgft  3516  elabgtOLD  3627  reupick  4275  reusv3  5367  sbcop1  5458  propeqop  5479  pwssun  5543  wefrc  5645  ssrel  5759  ssrel2  5761  ssrelrel  5772  ssrelrn  5876  tz7.7  6387  ordtr2  6407  onmindif  6456  unizlim  6486  funssres  6582  f1ssf1  6855  fvmptt  7012  fveqdmss  7076  fvcofneq  7091  funsndifnop  7153  funfvima2  7235  isoini  7344  isopolem  7351  weniso  7362  f1ocnv2d  7672  limsssuc  7859  tfindsg  7870  limomss  7880  findsg  7907  funcnvuni  7942  f1oweALT  7982  funelss  8056  bropopvvv  8099  bropfvvvvlem  8100  bropfvvvv  8101  f1o2ndf1  8131  frxp  8136  soseq  8169  suppfnss  8199  onfununi  8342  tz7.48lem  8443  tz7.49  8448  omordi  8567  omlimcl  8579  omass  8581  oeordsuc  8596  nnmordi  8633  nnmord  8634  omabs  8653  xpdom2  9084  infensuc  9167  findcard2  9173  findcard2d  9175  findcard3  9267  frfi  9269  fsuppres  9378  dffi2  9408  elfiun  9415  ordiso2  9502  ordtypelem7  9511  suc11reg  9613  inf3lem2  9623  noinfep  9654  cantnfle  9665  cantnflem1  9683  cantnf  9687  ttrclss  9714  trcl  9722  epfrs  9725  frr3g  9753  r1sdom  9774  setrec1lem2  9960  updjud  10008  dfac8alem  10101  indcardi  10113  alephordi  10146  dfac12lem3  10217  pwsdompw  10274  cofsmo  10340  cfcoflem  10343  coftr  10344  isf32lem2  10425  isf32lem9  10432  axcc3  10509  domtriomlem  10513  axdc3lem2  10522  axdc3lem4  10524  zorn2lem4  10570  zorn2lem6  10572  zorn2lem7  10573  ttukeylem6  10585  uniimadom  10621  konigthlem  10646  fpwwe2lem7  10715  tskord  10858  tskcard  10859  grupr  10875  gruiin  10888  grudomon  10895  grur1a  10897  genpn0  11081  genpcd  11084  distrlem5pr  11105  psslinpr  11109  ltaddpr  11112  ltexprlem3  11116  ltexprlem6  11119  ltapr  11123  prlem936  11125  suplem1pr  11130  axpre-sup  11247  1re  11301  dedekindle  11467  lemul12a  12168  divgt0  12178  divge0  12179  lbreu  12260  sup2  12266  bndndx  12598  elnnz  12696  nzadd  12737  fzind  12790  fnn0ind  12791  uzwo  13031  lbzbi  13056  zmax  13065  zbtwnre  13066  irradd  13094  irrmul  13095  ledivge1le  13186  xrub  13435  supxrunb2  13443  infmremnf  13467  iccid  13514  uzsubsubfz  13673  fzrevral  13739  elfz0fzfz0  13760  fz0fzelfz0  13761  elfzmlbp  13766  elincfzoext  13851  ssfzoulel  13888  ssfzo12bi  13889  fzoopth  13890  elfzonelfzo  13897  elfznelfzo  13901  elfznelfzob  13902  injresinjlem  13918  fleqceilz  13987  modaddmodup  14070  uzindi  14118  suppssfz  14130  mptnn0fsuppr  14135  le2sq2  14271  sqlecan  14346  facdiv  14424  facwordi  14426  faclbnd  14427  hashimarni  14579  hash2prd  14613  hashle2pr  14615  pr2pwpr  14617  fundmge2nop0  14640  fi1uzind  14645  brfi1indALT  14648  swrdnd2  14798  swrdnnn0nd  14799  swrdnd0  14800  pfxnd0  14831  swrdswrdlem  14846  swrdswrd  14847  ccatopth2  14859  wrd2ind  14865  pfxccatin12lem2a  14869  swrdccatin2  14871  pfxccatin12lem2  14873  pfxccatin12lem3  14874  swrdccat  14877  swrdccat3blem  14881  reuccatpfxs1lem  14888  repswswrd  14928  cshwidxmod  14947  cshwidx0  14950  2cshwcshw  14969  cshwcsh2id  14972  cau3lem  15515  caubnd  15519  climrlim2  15707  rlimcn3  15750  mulcn2  15756  climcau  15831  climbdd  15832  caucvg  15839  modfsummod  15954  p1modz1  16422  dvdsle  16473  dvdsdivcl  16479  ltoddhalfle  16524  halfleoddlt  16525  ndvdssub  16572  gcdcllem1  16662  dvdslegcd  16667  bezoutlem4  16708  dfgcd2  16712  lcmf  16801  lcmfunsnlem1  16805  lcmfunsnlem2lem1  16806  lcmfunsnlem  16809  lcmfdvdsb  16811  lcmfun  16813  coprmdvds1  16820  divgcdcoprm0  16833  cncongr1  16835  cncongr2  16836  prmfac1  16889  pcqcl  17027  dvdsprmpweqle  17057  oddprmdvds  17074  prmpwdvds  17075  infpnlem1  17081  prmgaplem5  17226  prmgaplem6  17227  prmgaplem7  17228  cshwshashlem1  17266  cictr  17973  initoeu2lem1  18182  initoeu2  18184  clatleglb  18685  lidrididd  18844  mulgaddcom  19301  mulginvcom  19302  cycsubm  19410  cyccom  19411  gsmsymgreqlem2  19638  symggen  19677  psgnunilem4  19704  sylow2blem3  19829  frgpnabllem1  20080  imasabl  20083  dprddisj2  20248  lmodfopnelem1  21166  lssssr  21222  lss1d  21231  lspsncv0  21417  rnglidlmcl  21488  lidlunin0  21508  unichnlidl  21509  rngqiprngimfo  21590  nzerooringczr  21779  pzriprnglem5  21784  pzriprnglem8  21787  znrrg  21864  mplcoe5lem  22341  cply1mul  22607  coe1fzgsumdlem  22614  gsummoncoe1  22619  evl1gsumdlem  22667  mamufacex  22704  dmatelnd  22804  scmataddcl  22824  scmatsubcl  22825  scmatmulcl  22826  smatvscl  22832  mavmulsolcl  22859  mdetdiagid  22908  matunitlindflem1  22987  matunitlindflem2  22988  cramerlem3  23000  pmatcoe1fsupp  23012  cpmatacl  23027  cpmatmcllem  23029  mp2pm2mplem4  23120  chpscmat  23153  chfacfisf  23165  chfacfisfcpmat  23166  uniopn  23208  opnnei  23431  neindisj2  23434  restcls  23492  restntr  23493  tgcnp  23564  subbascn  23565  iscnp4  23574  lpcls  23675  cmpsublem  23710  cmpsub  23711  tgcmp  23712  cmpcld  23713  dfconn2  23730  1stcrest  23764  2ndcdisj  23768  1stccnp  23774  comppfsc  23844  kgencn2  23869  txlm  23960  kqreglem1  24053  filin  24166  isfil2  24168  ufilmax  24219  ufileu  24231  filufint  24232  cfinufil  24240  elfm2  24260  rnelfmlem  24264  rnelfm  24265  flimopn  24287  fbflim2  24289  flffbas  24307  fclsnei  24331  flimfnfcls  24340  fclscmp  24342  fcfnei  24347  cnpfcf  24353  alexsubALTlem2  24360  alexsubALTlem3  24361  alexsubALTlem4  24362  alexsubALT  24363  ptcmplem4  24367  qustgplem  24433  tsmsres  24456  tsmsxp  24467  metss  24820  metcnp3  24852  ovoliunnul  25821  ovolicc2lem3  25833  dyadmax  25912  itg2le  26053  bddiblnc  26155  itgcn  26158  ellimc3  26192  lhop1  26327  dvfsumrlim  26344  fta1g  26481  dvply2g  26599  fta1  26622  aalioulem3  26654  aalioulem4  26655  ulmcaulem  26714  ulmcau  26715  logbgcd1irr  27115  xrlimcnp  27289  cxploglim  27298  jensen  27309  lgsqrmodndvds  27673  gausslemma2dlem1a  27685  gausslemma2dlem2  27687  gausslemma2dlem3  27688  lgsquad2lem2  27705  2lgslem1a1  27709  2sqlem6  27743  2sq2  27753  2sqnn  27759  2sqreultblem  27768  fltoprm  27988  fltoprmgt3  27989  nosepdmlem  28033  nodenselem8  28041  eqcuts3  28183  madebdaylemlrcut  28278  addsprop  28355  addsuniflem  28380  negsprop  28414  mulsprop  28509  mulsuniflem  28528  precsex  28597  onsfi  28735  elnnzs  28780  elreno2  28874  brbtwn2  29476  ax5seglem5  29504  axcontlem4  29538  axcontlem10  29544  umgrnloopv  29677  umgrnloop  29679  upgredgpr  29713  numedglnl  29715  usgrausgrb  29743  usgrnloopvALT  29775  usgrnloopALT  29777  usgredg2vlem2  29800  ushgredgedg  29803  ushgredgedgloop  29805  upgrreslem  29878  umgrreslem  29879  nbgr0edglem  29930  nbusgrvtxm1  29953  uvtxnbgrvtx  29967  cusgredg  29998  cusgrres  30022  cusgrsize2inds  30027  cusgrfi  30032  fusgrregdegfi  30143  ewlkle  30179  uspgr2wlkeqi  30221  lfgrwlkprop  30263  lfgrwlknloop  30265  pthdivtx  30305  2pthnloop  30310  upgrwlkdvdelem  30315  upgrspthswlk  30317  usgr2wlkneq  30335  usgr2trlncl  30339  usgr2pthlem  30342  usgr2pth  30343  uspgrn2crct  30390  crctcshwlkn0lem4  30395  crctcshwlkn0lem5  30396  crctcshwlkn0  30403  wlkiswwlks1  30449  wlkiswwlks2  30457  wlkiswwlksupgr2  30459  wwlksnred  30474  wwlksnext  30475  wwlksnextbi  30476  wwlksnextwrd  30479  wwlksnextinj  30481  wwlksnextproplem2  30492  wwlksnextproplem3  30493  wspthsnonn0vne  30499  wspn0  30506  2pthon3v  30525  usgrwwlks2on  30540  umgrwwlks2on  30541  elwspths2on  30544  elwspths2onw  30545  wpthswwlks2on  30546  clwwlk1loop  30572  clwwlkccatlem  30573  umgrclwwlkge2  30575  clwlkclwwlklem2a4  30581  clwlkclwwlklem2a  30582  clwlkclwwlklem3  30585  clwlkclwwlkf1lem3  30590  clwlkclwwlkfo  30593  clwwisshclwwslemlem  30597  erclwwlkeqlen  30603  erclwwlksym  30605  clwwlkf  30631  clwwlknscsh  30646  erclwwlknsym  30654  clwwlknonex2lem2  30692  clwwlknonex2  30693  umgr2cycllem  30739  upgr3v3e3cycl  30774  upgr4cycl4dv4e  30779  eucrctshift  30837  3vfriswmgr  30872  1to2vfriswmgr  30873  1to3vfriswmgr  30874  n4cyclfrgr  30885  4cyclusnfrgr  30886  frgrnbnb  30887  frgrncvvdeqlem8  30900  frgrwopreg  30917  frgr2wwlk1  30923  frgr2wwlkeqm  30925  2clwwlk2clwwlklem  30940  numclwwlk1lem2fo  30952  wlkl0  30961  numclwlk2lem2f  30971  frgrreggt1  30987  frgrreg  30988  frgrregord013  30989  frgrregord13  30990  frgrogt3nreg  30991  eulplig  31080  nmoub3i  31368  ipasslem5  31430  htthlem  31512  ocin  31891  spansneleq  32165  spansnss  32166  elspansn4  32168  h1datomi  32176  nmopub2tALT  32504  nmfnleub2  32521  hstel2  32814  cvnbtwn  32881  spansncv2  32888  dmdmd  32895  dmdbr3  32900  dmdbr4  32901  dmdbr5  32903  mdsl0  32905  mdexchi  32930  cvexchlem  32963  atcv1  32975  atomli  32977  atcvatlem  32980  atcvat2i  32982  chirredi  32989  mdsymlem3  33000  mdsymlem4  33001  sumdmdii  33010  sumdmdlem  33013  cdj1i  33028  ssrelf  33202  f1o3d  33213  fisshasheq  35882  cvxpconn  35986  satfv0  36102  satfsschain  36108  satfrel  36111  satfdm  36113  satfv0fun  36115  sat1el2xp  36123  gonarlem  36138  goalrlem  36140  satffunlem1lem1  36146  satffunlem2lem1  36148  satffunlem2lem2  36150  satffun  36153  mrsubccat  36262  msubvrs  36304  fundmpss  36511  dfon2lem6  36530  dfon2lem8  36532  dfon2lem9  36533  dfon2  36534  wzel  36566  colinearxfr  36820  btwnconn1lem11  36842  lineintmo  36902  in-ax8  36993  ss-ax8  36994  trer  37084  elicc3  37085  finminlem  37086  nn0prpwlem  37090  fnessref  37125  neibastop2  37129  fgmin  37138  tailfb  37145  ordcmp  37215  ee7.2aOLD  37229  dfttc4  37298  bj-ceqsalt0  37776  bj-ceqsalt1  37777  isbasisrelowllem1  38258  isbasisrelowllem2  38259  relowlpssretop  38267  fvineqsneu  38314  fvineqsneq  38315  wl-mo3t  38488  finixpnum  38508  poimirlem26  38544  poimirlem27  38545  poimirlem29  38547  ftc1anc  38599  fdc  38659  heibor1lem  38723  ghomco  38805  rngoueqz  38854  unichnidl  38945  dmncan1  38990  ax12indn  39980  lshpdisj  40024  lub0N  40226  glb0N  40230  leat2  40331  hlrelat2  40440  cvrexchlem  40456  cvratlem  40458  atcvrj0  40465  cvrat2  40466  snatpsubN  40787  linepsubN  40789  pmaple  40798  pmapsub  40805  elpaddn0  40837  paddasslem5  40861  trlval2  41200  cdlemn11pre  42247  dihord2pre  42262  mapdordlem2  42674  sn-sup2  43535  fsuppind  43598  pell1qrgap  43860  dford3lem1  44012  hbtlem5  44114  onexlimgt  44229  onsucf1olem  44256  omcl2  44319  tfsconcat0b  44332  ntrneiiso  45076  sbiota1  45403  19.41rg  45518  ee223  45602  or2expropbilem1  48071  funressnfv  48082  fcoresf1  48108  2reuimp  48154  f1oresf1o2  48330  zm1nn  48341  nltle2tri  48352  el1fzopredsuc  48365  modlt0b  48408  mod2addne  48409  muldvdsfacgt  48425  muldvdsfacm1  48426  elsetpreimafvssdm  48437  imasetpreimafvbijlemf1  48455  iccpartlt  48475  iccpartgt  48478  iccelpart  48484  icceuelpart  48487  iccpartnel  48489  fargshiftfo  48493  fargshiftfva  48494  lswn0  48495  ich2exprop  48522  prsprel  48538  sprsymrelfolem2  48544  sprsymrelfo  48548  poprelb  48575  reuopreuprim  48577  goldbachthlem2  48600  odz2prm2pw  48617  fmtnoprmfac1  48619  fmtnofac2lem  48622  prmdvdsfmtnof1lem2  48639  2pwp1prm  48643  sfprmdvdsmersenne  48657  lighneallem3  48661  requad01  48688  requad2  48690  even3prm2  48786  fppr2odd  48798  fpprwpprb  48807  gbegt5  48828  sbgoldbwt  48844  sbgoldbalt  48848  sbgoldbm  48851  bgoldbtbndlem2  48873  bgoldbtbndlem3  48874  bgoldbtbndlem4  48875  bgoldbtbnd  48876  tgblthelfgott  48882  tgoldbach  48884  isubgredg  48933  grimuhgr  48954  grimcnv  48955  grimco  48956  isuspgrim0  48961  isuspgrimlem  48962  uhgrimisgrgriclem  48997  clnbgrgrimlem  49000  grimedg  49002  grtriprop  49008  cycl3grtri  49014  grimgrtri  49016  isubgr3stgrlem6  49038  uspgrlimlem3  49057  uspgrlimlem4  49058  grlimgrtrilem2  49069  grlicsym  49080  clnbgr3stgrgrlim  49086  clnbgr3stgrgrlic  49087  gpgedg2ov  49133  gpgedg2iv  49134  pgnbgreunbgrlem3  49185  pgnbgreunbgrlem6  49191  upgrwlkupwlk  49207  lmod0rng  49295  idomcanl  49413  ztprmneprm  49428  ply1mulgsumlem1  49467  ply1mulgsumlem2  49468  lcoel0  49509  linindslinci  49529  lindslinindimp2lem4  49542  lindslinindsimp2lem5  49543  snlindsntor  49552  ldepspr  49554  lincresunit2  49559  fllog2  49649  dignn0ldlem  49683  dignn0flhalflem1  49696  nn0sumshdiglemA  49700  nn0sumshdiglemB  49701  itcovalt2  49758  resum2sqorgt0  49790  eenglngeehlnmlem2  49819  rrx2linest  49823  itscnhlc0xyqsol  49846  itsclc0  49852  aacllem  50908