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  1060  sbequ1  2284  moexexlem  2654  ralrimdvva  3220  ceqsal1t  3487  ceqsalt  3488  spcimgft  3515  vtoclgft  3520  elabgtOLD  3632  reupick  4282  reusv3  5376  sbcop1  5470  propeqop  5490  pwssun  5553  wefrc  5655  ssrel  5769  ssrel2  5771  ssrelrel  5782  ssrelrn  5884  tz7.7  6386  ordtr2  6406  onmindif  6455  unizlim  6485  funssres  6580  f1ssf1  6853  fvmptt  7010  fveqdmss  7073  fvcofneq  7088  funsndifnop  7148  funfvima2  7229  isoini  7336  isopolem  7343  weniso  7352  f1ocnv2d  7663  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  10248  cfcoflem  10251  coftr  10252  isf32lem2  10333  isf32lem9  10340  axcc3  10417  domtriomlem  10421  axdc3lem2  10430  axdc3lem4  10432  zorn2lem4  10478  zorn2lem6  10480  zorn2lem7  10481  ttukeylem6  10493  uniimadom  10523  konigthlem  10548  fpwwe2lem7  10617  tskord  10760  tskcard  10761  grupr  10777  gruiin  10790  grudomon  10797  grur1a  10799  genpn0  10983  genpcd  10986  distrlem5pr  11007  psslinpr  11011  ltaddpr  11014  ltexprlem3  11018  ltexprlem6  11021  ltapr  11025  prlem936  11027  suplem1pr  11032  axpre-sup  11149  1re  11203  dedekindle  11369  lemul12a  12068  divgt0  12078  divge0  12079  lbreu  12160  sup2  12166  bndndx  12498  elnnz  12596  nzadd  12637  fzind  12689  fnn0ind  12690  uzwo  12930  lbzbi  12955  zmax  12964  zbtwnre  12965  irradd  12992  irrmul  12993  ledivge1le  13084  xrub  13333  supxrunb2  13341  infmremnf  13365  iccid  13412  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  16312  dvdsle  16363  dvdsdivcl  16369  ltoddhalfle  16414  halfleoddlt  16415  ndvdssub  16462  gcdcllem1  16552  dvdslegcd  16557  bezoutlem4  16595  dfgcd2  16599  lcmf  16686  lcmfunsnlem1  16690  lcmfunsnlem2lem1  16691  lcmfunsnlem  16694  lcmfdvdsb  16696  lcmfun  16698  coprmdvds1  16705  divgcdcoprm0  16718  cncongr1  16720  cncongr2  16721  prmfac1  16774  pcqcl  16911  dvdsprmpweqle  16941  oddprmdvds  16958  prmpwdvds  16959  infpnlem1  16965  prmgaplem5  17110  prmgaplem6  17111  prmgaplem7  17112  cshwshashlem1  17150  cictr  17857  initoeu2lem1  18066  initoeu2  18068  clatleglb  18569  lidrididd  18723  mulgaddcom  19159  mulginvcom  19160  cycsubm  19268  cyccom  19269  gsmsymgreqlem2  19496  symggen  19535  psgnunilem4  19562  sylow2blem3  19687  frgpnabllem1  19938  imasabl  19941  dprddisj2  20106  lmodfopnelem1  21019  lssssr  21075  lss1d  21084  lspsncv0  21270  rnglidlmcl  21341  lidlunin0  21361  unichnlidl  21362  rngqiprngimfo  21441  nzerooringczr  21630  pzriprnglem5  21635  pzriprnglem8  21638  znrrg  21715  mplcoe5lem  22190  cply1mul  22456  coe1fzgsumdlem  22463  gsummoncoe1  22468  evl1gsumdlem  22516  mamufacex  22553  dmatelnd  22653  scmataddcl  22673  scmatsubcl  22674  scmatmulcl  22675  smatvscl  22681  mavmulsolcl  22708  mdetdiagid  22757  cramerlem3  22846  pmatcoe1fsupp  22858  cpmatacl  22873  cpmatmcllem  22875  mp2pm2mplem4  22966  chpscmat  22999  chfacfisf  23011  chfacfisfcpmat  23012  uniopn  23054  opnnei  23277  neindisj2  23280  restcls  23338  restntr  23339  tgcnp  23410  subbascn  23411  iscnp4  23420  lpcls  23521  cmpsublem  23556  cmpsub  23557  tgcmp  23558  cmpcld  23559  dfconn2  23576  1stcrest  23610  2ndcdisj  23613  1stccnp  23619  comppfsc  23689  kgencn2  23714  txlm  23805  kqreglem1  23898  filin  24011  isfil2  24013  ufilmax  24064  ufileu  24076  filufint  24077  cfinufil  24085  elfm2  24105  rnelfmlem  24109  rnelfm  24110  flimopn  24132  fbflim2  24134  flffbas  24152  fclsnei  24176  flimfnfcls  24185  fclscmp  24187  fcfnei  24192  cnpfcf  24198  alexsubALTlem2  24205  alexsubALTlem3  24206  alexsubALTlem4  24207  alexsubALT  24208  ptcmplem4  24212  qustgplem  24278  tsmsres  24301  tsmsxp  24312  metss  24665  metcnp3  24697  ovoliunnul  25666  ovolicc2lem3  25678  dyadmax  25757  itg2le  25898  bddiblnc  26001  itgcn  26004  ellimc3  26038  lhop1  26173  dvfsumrlim  26190  fta1g  26327  dvply2g  26446  fta1  26469  aalioulem3  26497  aalioulem4  26498  ulmcaulem  26557  ulmcau  26558  logbgcd1irr  26959  xrlimcnp  27133  cxploglim  27142  jensen  27153  lgsqrmodndvds  27517  gausslemma2dlem1a  27529  gausslemma2dlem2  27531  gausslemma2dlem3  27532  lgsquad2lem2  27549  2lgslem1a1  27553  2sqlem6  27587  2sq2  27597  2sqnn  27603  2sqreultblem  27612  nosepdmlem  27847  nodenselem8  27855  eqcuts3  27997  madebdaylemlrcut  28092  addsprop  28169  addsuniflem  28194  negsprop  28228  mulsprop  28323  mulsuniflem  28342  precsex  28411  onsfi  28549  elnnzs  28594  elreno2  28688  brbtwn2  29255  ax5seglem5  29283  axcontlem4  29317  axcontlem10  29323  umgrnloopv  29456  umgrnloop  29458  upgredgpr  29492  numedglnl  29494  usgrausgrb  29519  usgrnloopvALT  29551  usgrnloopALT  29553  usgredg2vlem2  29576  ushgredgedg  29579  ushgredgedgloop  29581  upgrreslem  29654  umgrreslem  29655  nbgr0edglem  29706  nbusgrvtxm1  29729  uvtxnbgrvtx  29743  cusgredg  29774  cusgrres  29798  cusgrsize2inds  29803  cusgrfi  29808  fusgrregdegfi  29919  ewlkle  29955  uspgr2wlkeqi  29997  lfgrwlkprop  30035  lfgrwlknloop  30037  pthdivtx  30076  2pthnloop  30080  upgrwlkdvdelem  30085  upgrspthswlk  30087  usgr2wlkneq  30105  usgr2trlncl  30109  usgr2pthlem  30112  usgr2pth  30113  uspgrn2crct  30157  crctcshwlkn0lem4  30162  crctcshwlkn0lem5  30163  crctcshwlkn0  30170  wlkiswwlks1  30216  wlkiswwlks2  30224  wlkiswwlksupgr2  30226  wwlksnred  30241  wwlksnext  30242  wwlksnextbi  30243  wwlksnextwrd  30246  wwlksnextinj  30248  wwlksnextproplem2  30259  wwlksnextproplem3  30260  wspthsnonn0vne  30266  wspn0  30273  2pthon3v  30292  usgrwwlks2on  30307  umgrwwlks2on  30308  elwspths2on  30311  elwspths2onw  30312  wpthswwlks2on  30313  clwwlk1loop  30339  clwwlkccatlem  30340  umgrclwwlkge2  30342  clwlkclwwlklem2a4  30348  clwlkclwwlklem2a  30349  clwlkclwwlklem3  30352  clwlkclwwlkf1lem3  30357  clwlkclwwlkfo  30360  clwwisshclwwslemlem  30364  erclwwlkeqlen  30370  erclwwlksym  30372  clwwlkf  30398  clwwlknscsh  30413  erclwwlknsym  30421  clwwlknonex2lem2  30459  clwwlknonex2  30460  upgr3v3e3cycl  30531  upgr4cycl4dv4e  30536  eucrctshift  30594  3vfriswmgr  30629  1to2vfriswmgr  30630  1to3vfriswmgr  30631  n4cyclfrgr  30642  4cyclusnfrgr  30643  frgrnbnb  30644  frgrncvvdeqlem8  30657  frgrwopreg  30674  frgr2wwlk1  30680  frgr2wwlkeqm  30682  2clwwlk2clwwlklem  30697  numclwwlk1lem2fo  30709  wlkl0  30718  numclwlk2lem2f  30728  frgrreggt1  30744  frgrreg  30745  frgrregord013  30746  frgrregord13  30747  frgrogt3nreg  30748  eulplig  30837  nmoub3i  31125  ipasslem5  31187  htthlem  31269  ocin  31648  spansneleq  31922  spansnss  31923  elspansn4  31925  h1datomi  31933  nmopub2tALT  32261  nmfnleub2  32278  hstel2  32571  cvnbtwn  32638  spansncv2  32645  dmdmd  32652  dmdbr3  32657  dmdbr4  32658  dmdbr5  32660  mdsl0  32662  mdexchi  32687  cvexchlem  32720  atcv1  32732  atomli  32734  atcvatlem  32737  atcvat2i  32739  chirredi  32746  mdsymlem3  32757  mdsymlem4  32758  sumdmdii  32767  sumdmdlem  32770  cdj1i  32785  ssrelf  32960  f1o3d  32971  fisshasheq  35606  umgr2cycllem  35632  cvxpconn  35734  satfv0  35850  satfsschain  35856  satfrel  35859  satfdm  35861  satfv0fun  35863  sat1el2xp  35871  gonarlem  35886  goalrlem  35888  satffunlem1lem1  35894  satffunlem2lem1  35896  satffunlem2lem2  35898  satffun  35901  mrsubccat  36010  msubvrs  36052  fundmpss  36259  dfon2lem6  36278  dfon2lem8  36280  dfon2lem9  36281  dfon2  36282  wzel  36314  colinearxfr  36567  btwnconn1lem11  36589  lineintmo  36649  in-ax8  36736  ss-ax8  36737  trer  36827  elicc3  36828  finminlem  36829  nn0prpwlem  36833  fnessref  36868  neibastop2  36872  fgmin  36881  tailfb  36888  ordcmp  36958  ee7.2aOLD  36972  dfttc4  37041  bj-ceqsalt0  37519  bj-ceqsalt1  37520  isbasisrelowllem1  38001  isbasisrelowllem2  38002  relowlpssretop  38010  fvineqsneu  38057  fvineqsneq  38058  wl-mo3t  38231  finixpnum  38256  matunitlindflem1  38267  matunitlindflem2  38268  poimirlem26  38297  poimirlem27  38298  poimirlem29  38300  ftc1anc  38352  fdc  38396  heibor1lem  38460  ghomco  38542  rngoueqz  38591  unichnidl  38682  dmncan1  38727  ax12indn  39717  lshpdisj  39761  lub0N  39963  glb0N  39967  leat2  40068  hlrelat2  40177  cvrexchlem  40193  cvratlem  40195  atcvrj0  40202  cvrat2  40203  snatpsubN  40524  linepsubN  40526  pmaple  40535  pmapsub  40542  elpaddn0  40574  paddasslem5  40598  trlval2  40937  cdlemn11pre  41984  dihord2pre  41999  mapdordlem2  42411  sn-sup2  43265  fsuppind  43322  pell1qrgap  43601  dford3lem1  43753  hbtlem5  43855  onexlimgt  43970  onsucf1olem  43997  omcl2  44060  tfsconcat0b  44073  ntrneiiso  44817  sbiota1  45144  19.41rg  45259  ee223  45343  or2expropbilem1  47769  funressnfv  47780  fcoresf1  47806  2reuimp  47852  f1oresf1o2  48028  zm1nn  48039  nltle2tri  48050  el1fzopredsuc  48063  modlt0b  48106  mod2addne  48107  muldvdsfacgt  48123  muldvdsfacm1  48124  elsetpreimafvssdm  48135  imasetpreimafvbijlemf1  48153  iccpartlt  48173  iccpartgt  48176  iccelpart  48182  icceuelpart  48185  iccpartnel  48187  fargshiftfo  48191  fargshiftfva  48192  lswn0  48193  ich2exprop  48220  prsprel  48236  sprsymrelfolem2  48242  sprsymrelfo  48246  poprelb  48273  reuopreuprim  48275  goldbachthlem2  48298  odz2prm2pw  48315  fmtnoprmfac1  48317  fmtnofac2lem  48320  prmdvdsfmtnof1lem2  48337  2pwp1prm  48341  sfprmdvdsmersenne  48355  lighneallem3  48359  requad01  48386  requad2  48388  even3prm2  48484  fppr2odd  48496  fpprwpprb  48505  gbegt5  48526  sbgoldbwt  48542  sbgoldbalt  48546  sbgoldbm  48549  bgoldbtbndlem2  48571  bgoldbtbndlem3  48572  bgoldbtbndlem4  48573  bgoldbtbnd  48574  tgblthelfgott  48580  tgoldbach  48582  isubgredg  48631  grimuhgr  48652  grimcnv  48653  grimco  48654  isuspgrim0  48659  isuspgrimlem  48660  uhgrimisgrgriclem  48695  clnbgrgrimlem  48698  grimedg  48700  grtriprop  48706  cycl3grtri  48712  grimgrtri  48714  isubgr3stgrlem6  48736  uspgrlimlem3  48755  uspgrlimlem4  48756  grlimgrtrilem2  48767  grlicsym  48778  clnbgr3stgrgrlim  48784  clnbgr3stgrgrlic  48785  gpgedg2ov  48831  gpgedg2iv  48832  pgnbgreunbgrlem3  48883  pgnbgreunbgrlem6  48889  upgrwlkupwlk  48905  lmod0rng  48994  idomcanl  49112  ztprmneprm  49127  ply1mulgsumlem1  49166  ply1mulgsumlem2  49167  lcoel0  49208  linindslinci  49228  lindslinindimp2lem4  49241  lindslinindsimp2lem5  49242  snlindsntor  49251  ldepspr  49253  lincresunit2  49258  fllog2  49348  dignn0ldlem  49382  dignn0flhalflem1  49395  nn0sumshdiglemA  49399  nn0sumshdiglemB  49400  itcovalt2  49457  resum2sqorgt0  49489  eenglngeehlnmlem2  49518  rrx2linest  49522  itscnhlc0xyqsol  49545  itsclc0  49551  setrec1lem2  50466  aacllem  50621