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  415  expcomd  420  impancom  455  a2and  842  dedlem0b  1040  sbequ1  2246  moexexlem  2688  ralrimdvva  3159  ceqsalt  3474  vtoclgft  3501  vtoclgftOLD  3502  sbciegft  3756  reupick  4239  reusv3  5271  sbcop1  5344  propeqop  5362  pwssun  5421  wefrc  5513  ssrel  5621  ssrel2  5623  ssrelrel  5633  ssrelrn  5727  predpo  6134  tz7.7  6185  ordtr2  6203  onmindif  6248  unizlim  6275  funssres  6368  f1ssf1  6621  fvmptt  6765  fveqdmss  6823  fvcofneq  6836  funsndifnop  6890  funfvima2  6971  isoini  7070  isopolem  7077  weniso  7086  f1ocnv2d  7378  limsssuc  7545  tfindsg  7555  limomss  7565  findsg  7590  funcnvuni  7618  f1oweALT  7655  funelss  7728  bropopvvv  7768  bropfvvvvlem  7769  bropfvvvv  7770  f1o2ndf1  7801  frxp  7803  suppfnss  7838  wfrlem12  7949  onfununi  7961  tz7.49  8064  omordi  8175  omlimcl  8187  omass  8189  oeordsuc  8203  nnmordi  8240  nnmord  8241  omabs  8257  xpdom2  8595  infensuc  8679  findcard2  8742  findcard2d  8744  findcard3  8745  frfi  8747  xpfi  8773  fsuppres  8842  dffi2  8871  elfiun  8878  ordiso2  8963  ordtypelem7  8972  suc11reg  9066  inf3lem2  9076  noinfep  9107  cantnfle  9118  cantnflem1  9136  cantnf  9140  trcl  9154  epfrs  9157  r1sdom  9187  updjud  9347  pr2ne  9416  dfac8alem  9440  indcardi  9452  alephordi  9485  dfac12lem3  9556  pwsdompw  9615  cofsmo  9680  cfcoflem  9683  coftr  9684  isf32lem2  9765  isf32lem9  9772  axcc3  9849  domtriomlem  9853  axdc3lem2  9862  axdc3lem4  9864  zorn2lem4  9910  zorn2lem6  9912  zorn2lem7  9913  ttukeylem6  9925  uniimadom  9955  konigthlem  9979  fpwwe2lem8  10048  tskord  10191  tskcard  10192  grupr  10208  gruiin  10221  grudomon  10228  grur1a  10230  genpn0  10414  genpcd  10417  distrlem5pr  10438  psslinpr  10442  ltaddpr  10445  ltexprlem3  10449  ltexprlem6  10452  ltapr  10456  prlem936  10458  suplem1pr  10463  axpre-sup  10580  1re  10630  dedekindle  10793  lemul12a  11487  divgt0  11497  divge0  11498  lbreu  11578  sup2  11584  bndndx  11884  elnnz  11979  nzadd  12018  fzind  12068  fnn0ind  12069  uzwo  12299  lbzbi  12324  zmax  12333  zbtwnre  12334  irradd  12360  irrmul  12361  ledivge1le  12448  xrub  12693  supxrunb2  12701  infmremnf  12724  iccid  12771  uzsubsubfz  12924  fzrevral  12987  elfz0fzfz0  13007  fz0fzelfz0  13008  elfzmlbp  13013  elincfzoext  13090  ssfzoulel  13126  ssfzo12bi  13127  elfzonelfzo  13134  elfznelfzo  13137  elfznelfzob  13138  injresinjlem  13152  fleqceilz  13217  modaddmodup  13297  uzindi  13345  suppssfz  13357  mptnn0fsuppr  13362  le2sq2  13496  sqlecan  13567  facdiv  13643  facwordi  13645  faclbnd  13646  hashimarni  13798  hash2prd  13829  hashle2pr  13831  pr2pwpr  13833  fundmge2nop0  13846  fi1uzind  13851  brfi1indALT  13854  swrdnd2  14008  swrdnnn0nd  14009  swrdnd0  14010  pfxnd0  14041  swrdswrdlem  14057  swrdswrd  14058  ccatopth2  14070  wrd2ind  14076  pfxccatin12lem2a  14080  swrdccatin2  14082  pfxccatin12lem2  14084  pfxccatin12lem3  14085  swrdccat  14088  swrdccat3blem  14092  reuccatpfxs1lem  14099  repswswrd  14137  cshwidxmod  14156  cshwidx0  14159  2cshwcshw  14178  cshwcsh2id  14181  cau3lem  14706  caubnd  14710  climrlim2  14896  rlimcn2  14939  mulcn2  14944  climcau  15019  climbdd  15020  caucvg  15027  modfsummod  15141  p1modz1  15606  dvdsle  15652  dvdsdivcl  15658  ltoddhalfle  15702  halfleoddlt  15703  ndvdssub  15750  gcdcllem1  15838  dvdslegcd  15843  bezoutlem4  15880  dfgcd2  15884  lcmf  15967  lcmfunsnlem1  15971  lcmfunsnlem2lem1  15972  lcmfunsnlem  15975  lcmfdvdsb  15977  lcmfun  15979  coprmdvds1  15986  divgcdcoprm0  15999  cncongr1  16001  cncongr2  16002  prmfac1  16053  pcqcl  16183  dvdsprmpweqle  16212  oddprmdvds  16229  prmpwdvds  16230  infpnlem1  16236  prmgaplem5  16381  prmgaplem6  16382  prmgaplem7  16383  cshwshashlem1  16421  cictr  17067  initoeu2lem1  17266  initoeu2  17268  clatleglb  17728  lidrididd  17872  mulgaddcom  18243  mulginvcom  18244  cycsubm  18337  cyccom  18338  gsmsymgreqlem2  18551  symggen  18590  psgnunilem4  18617  sylow2blem3  18739  frgpnabllem1  18986  dprddisj2  19154  f1rhm0to0ALT  19489  lmodfopnelem1  19663  lssssr  19718  lss1d  19728  lspsncv0  19911  znrrg  20257  mplcoe5lem  20707  cply1mul  20923  coe1fzgsumdlem  20930  gsummoncoe1  20933  evl1gsumdlem  20980  mamufacex  20996  dmatelnd  21101  scmataddcl  21121  scmatsubcl  21122  scmatmulcl  21123  smatvscl  21129  mavmulsolcl  21156  mdetdiagid  21205  cramerlem3  21294  pmatcoe1fsupp  21306  cpmatacl  21321  cpmatmcllem  21323  mp2pm2mplem4  21414  chpscmat  21447  chfacfisf  21459  chfacfisfcpmat  21460  uniopn  21502  opnnei  21725  neindisj2  21728  restcls  21786  restntr  21787  tgcnp  21858  subbascn  21859  iscnp4  21868  lpcls  21969  cmpsublem  22004  cmpsub  22005  tgcmp  22006  cmpcld  22007  dfconn2  22024  1stcrest  22058  2ndcdisj  22061  1stccnp  22067  comppfsc  22137  kgencn2  22162  txlm  22253  kqreglem1  22346  filin  22459  isfil2  22461  ufilmax  22512  ufileu  22524  filufint  22525  cfinufil  22533  elfm2  22553  rnelfmlem  22557  rnelfm  22558  flimopn  22580  fbflim2  22582  flffbas  22600  fclsnei  22624  flimfnfcls  22633  fclscmp  22635  fcfnei  22640  cnpfcf  22646  alexsubALTlem2  22653  alexsubALTlem3  22654  alexsubALTlem4  22655  alexsubALT  22656  ptcmplem4  22660  qustgplem  22726  tsmsres  22749  tsmsxp  22760  metss  23115  metcnp3  23147  ovoliunnul  24111  ovolicc2lem3  24123  dyadmax  24202  itg2le  24343  bddiblnc  24445  itgcn  24448  ellimc3  24482  lhop1  24617  dvfsumrlim  24634  fta1g  24768  fta1  24904  aalioulem3  24930  aalioulem4  24931  ulmcaulem  24989  ulmcau  24990  logbgcd1irr  25380  xrlimcnp  25554  cxploglim  25563  jensen  25574  lgsqrmodndvds  25937  gausslemma2dlem1a  25949  gausslemma2dlem2  25951  gausslemma2dlem3  25952  lgsquad2lem2  25969  2lgslem1a1  25973  2sqlem6  26007  2sq2  26017  2sqnn  26023  2sqreultblem  26032  brbtwn2  26699  ax5seglem5  26727  axcontlem4  26761  axcontlem10  26767  umgrnloopv  26899  umgrnloop  26901  upgredgpr  26935  numedglnl  26937  usgrausgrb  26962  usgrnloopvALT  26991  usgrnloopALT  26993  usgredg2vlem2  27016  ushgredgedg  27019  ushgredgedgloop  27021  upgrreslem  27094  umgrreslem  27095  nbgr0vtxlem  27145  nbusgrvtxm1  27169  uvtxnbgrvtx  27183  cusgredg  27214  cusgrres  27238  cusgrsize2inds  27243  cusgrfi  27248  fusgrregdegfi  27359  ewlkle  27395  uspgr2wlkeqi  27437  wlklenvclwlkOLD  27445  lfgrwlkprop  27477  lfgrwlknloop  27479  pthdivtx  27518  2pthnloop  27520  upgrwlkdvdelem  27525  upgrspthswlk  27527  usgr2wlkneq  27545  usgr2trlncl  27549  usgr2pthlem  27552  usgr2pth  27553  uspgrn2crct  27594  crctcshwlkn0lem4  27599  crctcshwlkn0lem5  27600  crctcshwlkn0  27607  wlkiswwlks1  27653  wlkiswwlks2  27661  wlkiswwlksupgr2  27663  wwlksnred  27678  wwlksnext  27679  wwlksnextbi  27680  wwlksnextwrd  27683  wwlksnextinj  27685  wwlksnextproplem2  27696  wwlksnextproplem3  27697  wspthsnonn0vne  27703  wspn0  27710  2pthon3v  27729  umgrwwlks2on  27743  elwspths2on  27746  wpthswwlks2on  27747  clwwlk1loop  27773  clwwlkccatlem  27774  umgrclwwlkge2  27776  clwlkclwwlklem2a4  27782  clwlkclwwlklem2a  27783  clwlkclwwlklem3  27786  clwlkclwwlkf1lem3  27791  clwlkclwwlkfo  27794  clwwisshclwwslemlem  27798  erclwwlkeqlen  27804  erclwwlksym  27806  clwwlkf  27832  clwwlknscsh  27847  erclwwlknsym  27855  clwwlknonex2lem2  27893  clwwlknonex2  27894  upgr3v3e3cycl  27965  upgr4cycl4dv4e  27970  eucrctshift  28028  3vfriswmgr  28063  1to2vfriswmgr  28064  1to3vfriswmgr  28065  n4cyclfrgr  28076  4cyclusnfrgr  28077  frgrnbnb  28078  frgrncvvdeqlem8  28091  frgrwopreg  28108  frgr2wwlk1  28114  frgr2wwlkeqm  28116  2clwwlk2clwwlklem  28131  numclwwlk1lem2fo  28143  wlkl0  28152  numclwlk2lem2f  28162  frgrreggt1  28178  frgrreg  28179  frgrregord013  28180  frgrregord13  28181  frgrogt3nreg  28182  eulplig  28268  nmoub3i  28556  ipasslem5  28618  htthlem  28700  ocin  29079  spansneleq  29353  spansnss  29354  elspansn4  29356  h1datomi  29364  nmopub2tALT  29692  nmfnleub2  29709  hstel2  30002  cvnbtwn  30069  spansncv2  30076  dmdmd  30083  dmdbr3  30088  dmdbr4  30089  dmdbr5  30091  mdsl0  30093  mdexchi  30118  cvexchlem  30151  atcv1  30163  atomli  30165  atcvatlem  30168  atcvat2i  30170  chirredi  30177  mdsymlem3  30188  mdsymlem4  30189  sumdmdii  30198  sumdmdlem  30201  cdj1i  30216  ssrelf  30379  f1o3d  30386  fisshasheq  32462  umgr2cycllem  32500  cvxpconn  32602  satfv0  32718  satfsschain  32724  satfrel  32727  satfdm  32729  satfv0fun  32731  sat1el2xp  32739  gonarlem  32754  goalrlem  32756  satffunlem1lem1  32762  satffunlem2lem1  32764  satffunlem2lem2  32766  satffun  32769  mrsubccat  32878  msubvrs  32920  fundmpss  33122  dfon2lem6  33146  dfon2lem8  33148  dfon2lem9  33149  dfon2  33150  trpredrec  33190  soseq  33209  wzel  33224  frr3g  33234  nosepdmlem  33300  nodenselem8  33308  colinearxfr  33649  btwnconn1lem11  33671  lineintmo  33731  trer  33777  elicc3  33778  finminlem  33779  nn0prpwlem  33783  fnessref  33818  neibastop2  33822  fgmin  33831  tailfb  33838  ordcmp  33908  ee7.2aOLD  33922  bj-cbvalimt  34085  bj-ceqsalt0  34324  bj-ceqsalt1  34325  isbasisrelowllem1  34772  isbasisrelowllem2  34773  relowlpssretop  34781  fvineqsneu  34828  fvineqsneq  34829  wl-mo3t  34977  finixpnum  35042  matunitlindflem1  35053  matunitlindflem2  35054  poimirlem26  35083  poimirlem27  35084  poimirlem29  35086  ftc1anc  35138  fdc  35183  heibor1lem  35247  ghomco  35329  rngoueqz  35378  unichnidl  35469  dmncan1  35514  ax12indn  36239  lshpdisj  36283  lub0N  36485  glb0N  36489  leat2  36590  hlrelat2  36699  cvrexchlem  36715  cvratlem  36717  atcvrj0  36724  cvrat2  36725  snatpsubN  37046  linepsubN  37048  pmaple  37057  pmapsub  37064  elpaddn0  37096  paddasslem5  37120  trlval2  37459  cdlemn11pre  38506  dihord2pre  38521  mapdordlem2  38933  fsuppind  39456  sn-sup2  39594  pell1qrgap  39815  dford3lem1  39967  hbtlem5  40072  ntrneiiso  40794  sbiota1  41138  19.41rg  41256  ee223  41340  or2expropbilem1  43624  funressnfv  43635  2reuimp  43671  f1oresf1o2  43847  zm1nn  43859  nltle2tri  43870  el1fzopredsuc  43882  fzoopth  43884  elsetpreimafvssdm  43903  imasetpreimafvbijlemf1  43921  iccpartlt  43941  iccpartgt  43944  iccelpart  43950  icceuelpart  43953  iccpartnel  43955  fargshiftfo  43959  fargshiftfva  43960  lswn0  43961  ich2exprop  43988  prsprel  44004  sprsymrelfolem2  44010  sprsymrelfo  44014  poprelb  44041  reuopreuprim  44043  goldbachthlem2  44063  odz2prm2pw  44080  fmtnoprmfac1  44082  fmtnofac2lem  44085  prmdvdsfmtnof1lem2  44102  2pwp1prm  44106  sfprmdvdsmersenne  44121  lighneallem3  44125  requad01  44139  requad2  44141  even3prm2  44237  fppr2odd  44249  fpprwpprb  44258  gbegt5  44279  sbgoldbwt  44295  sbgoldbalt  44299  sbgoldbm  44302  bgoldbtbndlem2  44324  bgoldbtbndlem3  44325  bgoldbtbndlem4  44326  bgoldbtbnd  44327  tgblthelfgott  44333  tgoldbach  44335  isomuspgrlem2b  44347  isomuspgrlem2d  44349  isomuspgr  44352  isomgrsym  44354  upgrwlkupwlk  44368  lmod0rng  44492  nzerooringczr  44696  ztprmneprm  44749  ply1mulgsumlem1  44794  ply1mulgsumlem2  44795  lcoel0  44837  linindslinci  44857  lindslinindimp2lem4  44870  lindslinindsimp2lem5  44871  snlindsntor  44880  ldepspr  44882  lincresunit2  44887  fllog2  44982  dignn0ldlem  45016  dignn0flhalflem1  45029  nn0sumshdiglemA  45033  nn0sumshdiglemB  45034  itcovalt2  45091  resum2sqorgt0  45123  eenglngeehlnmlem2  45152  rrx2linest  45156  itscnhlc0xyqsol  45179  itsclc0  45185  setrec1lem2  45218  aacllem  45329