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  413  expcomd  418  impancom  453  a2and  844  dedlem0b  1044  sbequ1  2241  moexexlem  2623  ralrimdvva  3210  ceqsal1t  3505  ceqsalt  3506  vtoclgft  3541  sbciegft  3815  reupick  4318  reusv3  5403  sbcop1  5488  propeqop  5507  pwssun  5571  wefrc  5670  ssrel  5781  ssrelOLD  5782  ssrel2  5784  ssrelrel  5795  ssrelrn  5893  tz7.7  6388  ordtr2  6406  onmindif  6454  unizlim  6485  funssres  6590  f1ssf1  6863  fvmptt  7016  fveqdmss  7078  fvcofneq  7092  funsndifnop  7146  funfvima2  7230  isoini  7332  isopolem  7339  weniso  7348  f1ocnv2d  7656  limsssuc  7836  tfindsg  7847  limomss  7857  findsg  7887  funcnvuni  7919  f1oweALT  7956  funelss  8030  bropopvvv  8073  bropfvvvvlem  8074  bropfvvvv  8075  f1o2ndf1  8105  frxp  8109  soseq  8142  suppfnss  8171  wfrlem12OLD  8317  onfununi  8338  tz7.49  8442  omordi  8563  omlimcl  8575  omass  8577  oeordsuc  8591  nnmordi  8628  nnmord  8629  omabs  8647  xpdom2  9064  infensuc  9152  findcard2  9161  findcard2d  9163  findcard2OLD  9281  findcard3  9282  findcard3OLD  9283  frfi  9285  xpfiOLD  9315  fsuppres  9385  dffi2  9415  elfiun  9422  ordiso2  9507  ordtypelem7  9516  suc11reg  9611  inf3lem2  9621  noinfep  9652  cantnfle  9663  cantnflem1  9681  cantnf  9685  ttrclss  9712  trcl  9720  epfrs  9723  frr3g  9748  r1sdom  9766  updjud  9926  pr2neOLD  9997  dfac8alem  10021  indcardi  10033  alephordi  10066  dfac12lem3  10137  pwsdompw  10196  cofsmo  10261  cfcoflem  10264  coftr  10265  isf32lem2  10346  isf32lem9  10353  axcc3  10430  domtriomlem  10434  axdc3lem2  10443  axdc3lem4  10445  zorn2lem4  10491  zorn2lem6  10493  zorn2lem7  10494  ttukeylem6  10506  uniimadom  10536  konigthlem  10560  fpwwe2lem7  10629  tskord  10772  tskcard  10773  grupr  10789  gruiin  10802  grudomon  10809  grur1a  10811  genpn0  10995  genpcd  10998  distrlem5pr  11019  psslinpr  11023  ltaddpr  11026  ltexprlem3  11030  ltexprlem6  11033  ltapr  11037  prlem936  11039  suplem1pr  11044  axpre-sup  11161  1re  11211  dedekindle  11375  lemul12a  12069  divgt0  12079  divge0  12080  lbreu  12161  sup2  12167  bndndx  12468  elnnz  12565  nzadd  12607  fzind  12657  fnn0ind  12658  uzwo  12892  lbzbi  12917  zmax  12926  zbtwnre  12927  irradd  12954  irrmul  12955  ledivge1le  13042  xrub  13288  supxrunb2  13296  infmremnf  13319  iccid  13366  uzsubsubfz  13520  fzrevral  13583  elfz0fzfz0  13603  fz0fzelfz0  13604  elfzmlbp  13609  elincfzoext  13687  ssfzoulel  13723  ssfzo12bi  13724  elfzonelfzo  13731  elfznelfzo  13734  elfznelfzob  13735  injresinjlem  13749  fleqceilz  13816  modaddmodup  13896  uzindi  13944  suppssfz  13956  mptnn0fsuppr  13961  le2sq2  14097  sqlecan  14170  facdiv  14244  facwordi  14246  faclbnd  14247  hashimarni  14398  hash2prd  14433  hashle2pr  14435  pr2pwpr  14437  fundmge2nop0  14450  fi1uzind  14455  brfi1indALT  14458  swrdnd2  14602  swrdnnn0nd  14603  swrdnd0  14604  pfxnd0  14635  swrdswrdlem  14651  swrdswrd  14652  ccatopth2  14664  wrd2ind  14670  pfxccatin12lem2a  14674  swrdccatin2  14676  pfxccatin12lem2  14678  pfxccatin12lem3  14679  swrdccat  14682  swrdccat3blem  14686  reuccatpfxs1lem  14693  repswswrd  14731  cshwidxmod  14750  cshwidx0  14753  2cshwcshw  14773  cshwcsh2id  14776  cau3lem  15298  caubnd  15302  climrlim2  15488  rlimcn3  15531  mulcn2  15537  climcau  15614  climbdd  15615  caucvg  15622  modfsummod  15737  p1modz1  16201  dvdsle  16250  dvdsdivcl  16256  ltoddhalfle  16301  halfleoddlt  16302  ndvdssub  16349  gcdcllem1  16437  dvdslegcd  16442  bezoutlem4  16481  dfgcd2  16485  lcmf  16567  lcmfunsnlem1  16571  lcmfunsnlem2lem1  16572  lcmfunsnlem  16575  lcmfdvdsb  16577  lcmfun  16579  coprmdvds1  16586  divgcdcoprm0  16599  cncongr1  16601  cncongr2  16602  prmfac1  16655  pcqcl  16786  dvdsprmpweqle  16816  oddprmdvds  16833  prmpwdvds  16834  infpnlem1  16840  prmgaplem5  16985  prmgaplem6  16986  prmgaplem7  16987  cshwshashlem1  17026  cictr  17749  initoeu2lem1  17961  initoeu2  17963  clatleglb  18468  lidrididd  18586  mulgaddcom  18973  mulginvcom  18974  cycsubm  19074  cyccom  19075  gsmsymgreqlem2  19294  symggen  19333  psgnunilem4  19360  sylow2blem3  19485  frgpnabllem1  19736  imasabl  19739  dprddisj2  19904  f1rhm0to0ALT  20273  lmodfopnelem1  20501  lssssr  20557  lss1d  20567  lspsncv0  20752  znrrg  21113  mplcoe5lem  21586  cply1mul  21810  coe1fzgsumdlem  21817  gsummoncoe1  21820  evl1gsumdlem  21867  mamufacex  21883  dmatelnd  21990  scmataddcl  22010  scmatsubcl  22011  scmatmulcl  22012  smatvscl  22018  mavmulsolcl  22045  mdetdiagid  22094  cramerlem3  22183  pmatcoe1fsupp  22195  cpmatacl  22210  cpmatmcllem  22212  mp2pm2mplem4  22303  chpscmat  22336  chfacfisf  22348  chfacfisfcpmat  22349  uniopn  22391  opnnei  22616  neindisj2  22619  restcls  22677  restntr  22678  tgcnp  22749  subbascn  22750  iscnp4  22759  lpcls  22860  cmpsublem  22895  cmpsub  22896  tgcmp  22897  cmpcld  22898  dfconn2  22915  1stcrest  22949  2ndcdisj  22952  1stccnp  22958  comppfsc  23028  kgencn2  23053  txlm  23144  kqreglem1  23237  filin  23350  isfil2  23352  ufilmax  23403  ufileu  23415  filufint  23416  cfinufil  23424  elfm2  23444  rnelfmlem  23448  rnelfm  23449  flimopn  23471  fbflim2  23473  flffbas  23491  fclsnei  23515  flimfnfcls  23524  fclscmp  23526  fcfnei  23531  cnpfcf  23537  alexsubALTlem2  23544  alexsubALTlem3  23545  alexsubALTlem4  23546  alexsubALT  23547  ptcmplem4  23551  qustgplem  23617  tsmsres  23640  tsmsxp  23651  metss  24009  metcnp3  24041  ovoliunnul  25016  ovolicc2lem3  25028  dyadmax  25107  itg2le  25249  bddiblnc  25351  itgcn  25354  ellimc3  25388  lhop1  25523  dvfsumrlim  25540  fta1g  25677  fta1  25813  aalioulem3  25839  aalioulem4  25840  ulmcaulem  25898  ulmcau  25899  logbgcd1irr  26289  xrlimcnp  26463  cxploglim  26472  jensen  26483  lgsqrmodndvds  26846  gausslemma2dlem1a  26858  gausslemma2dlem2  26860  gausslemma2dlem3  26861  lgsquad2lem2  26878  2lgslem1a1  26882  2sqlem6  26916  2sq2  26926  2sqnn  26932  2sqreultblem  26941  nosepdmlem  27176  nodenselem8  27184  madebdaylemlrcut  27383  addsprop  27450  addsuniflem  27474  negsprop  27499  mulsprop  27576  mulsuniflem  27594  precsex  27654  brbtwn2  28153  ax5seglem5  28181  axcontlem4  28215  axcontlem10  28221  umgrnloopv  28356  umgrnloop  28358  upgredgpr  28392  numedglnl  28394  usgrausgrb  28419  usgrnloopvALT  28448  usgrnloopALT  28450  usgredg2vlem2  28473  ushgredgedg  28476  ushgredgedgloop  28478  upgrreslem  28551  umgrreslem  28552  nbgr0vtxlem  28602  nbusgrvtxm1  28626  uvtxnbgrvtx  28640  cusgredg  28671  cusgrres  28695  cusgrsize2inds  28700  cusgrfi  28705  fusgrregdegfi  28816  ewlkle  28852  uspgr2wlkeqi  28895  lfgrwlkprop  28934  lfgrwlknloop  28936  pthdivtx  28976  2pthnloop  28978  upgrwlkdvdelem  28983  upgrspthswlk  28985  usgr2wlkneq  29003  usgr2trlncl  29007  usgr2pthlem  29010  usgr2pth  29011  uspgrn2crct  29052  crctcshwlkn0lem4  29057  crctcshwlkn0lem5  29058  crctcshwlkn0  29065  wlkiswwlks1  29111  wlkiswwlks2  29119  wlkiswwlksupgr2  29121  wwlksnred  29136  wwlksnext  29137  wwlksnextbi  29138  wwlksnextwrd  29141  wwlksnextinj  29143  wwlksnextproplem2  29154  wwlksnextproplem3  29155  wspthsnonn0vne  29161  wspn0  29168  2pthon3v  29187  umgrwwlks2on  29201  elwspths2on  29204  wpthswwlks2on  29205  clwwlk1loop  29231  clwwlkccatlem  29232  umgrclwwlkge2  29234  clwlkclwwlklem2a4  29240  clwlkclwwlklem2a  29241  clwlkclwwlklem3  29244  clwlkclwwlkf1lem3  29249  clwlkclwwlkfo  29252  clwwisshclwwslemlem  29256  erclwwlkeqlen  29262  erclwwlksym  29264  clwwlkf  29290  clwwlknscsh  29305  erclwwlknsym  29313  clwwlknonex2lem2  29351  clwwlknonex2  29352  upgr3v3e3cycl  29423  upgr4cycl4dv4e  29428  eucrctshift  29486  3vfriswmgr  29521  1to2vfriswmgr  29522  1to3vfriswmgr  29523  n4cyclfrgr  29534  4cyclusnfrgr  29535  frgrnbnb  29536  frgrncvvdeqlem8  29549  frgrwopreg  29566  frgr2wwlk1  29572  frgr2wwlkeqm  29574  2clwwlk2clwwlklem  29589  numclwwlk1lem2fo  29601  wlkl0  29610  numclwlk2lem2f  29620  frgrreggt1  29636  frgrreg  29637  frgrregord013  29638  frgrregord13  29639  frgrogt3nreg  29640  eulplig  29726  nmoub3i  30014  ipasslem5  30076  htthlem  30158  ocin  30537  spansneleq  30811  spansnss  30812  elspansn4  30814  h1datomi  30822  nmopub2tALT  31150  nmfnleub2  31167  hstel2  31460  cvnbtwn  31527  spansncv2  31534  dmdmd  31541  dmdbr3  31546  dmdbr4  31547  dmdbr5  31549  mdsl0  31551  mdexchi  31576  cvexchlem  31609  atcv1  31621  atomli  31623  atcvatlem  31626  atcvat2i  31628  chirredi  31635  mdsymlem3  31646  mdsymlem4  31647  sumdmdii  31656  sumdmdlem  31659  cdj1i  31674  ssrelf  31832  f1o3d  31839  fisshasheq  34093  umgr2cycllem  34120  cvxpconn  34222  satfv0  34338  satfsschain  34344  satfrel  34347  satfdm  34349  satfv0fun  34351  sat1el2xp  34359  gonarlem  34374  goalrlem  34376  satffunlem1lem1  34382  satffunlem2lem1  34384  satffunlem2lem2  34386  satffun  34389  mrsubccat  34498  msubvrs  34540  fundmpss  34727  dfon2lem6  34749  dfon2lem8  34751  dfon2lem9  34752  dfon2  34753  wzel  34785  colinearxfr  35036  btwnconn1lem11  35058  lineintmo  35118  trer  35190  elicc3  35191  finminlem  35192  nn0prpwlem  35196  fnessref  35231  neibastop2  35235  fgmin  35244  tailfb  35251  ordcmp  35321  ee7.2aOLD  35335  bj-cbvalimt  35505  bj-ceqsalt0  35753  bj-ceqsalt1  35754  isbasisrelowllem1  36225  isbasisrelowllem2  36226  relowlpssretop  36234  fvineqsneu  36281  fvineqsneq  36282  wl-mo3t  36430  finixpnum  36462  matunitlindflem1  36473  matunitlindflem2  36474  poimirlem26  36503  poimirlem27  36504  poimirlem29  36506  ftc1anc  36558  fdc  36602  heibor1lem  36666  ghomco  36748  rngoueqz  36797  unichnidl  36888  dmncan1  36933  ax12indn  37802  lshpdisj  37846  lub0N  38048  glb0N  38052  leat2  38153  hlrelat2  38263  cvrexchlem  38279  cvratlem  38281  atcvrj0  38288  cvrat2  38289  snatpsubN  38610  linepsubN  38612  pmaple  38621  pmapsub  38628  elpaddn0  38660  paddasslem5  38684  trlval2  39023  cdlemn11pre  40070  dihord2pre  40085  mapdordlem2  40497  fsuppind  41160  sn-sup2  41339  pell1qrgap  41598  dford3lem1  41751  hbtlem5  41856  onexlimgt  41978  onsucf1olem  42006  omcl2  42069  tfsconcat0b  42082  ntrneiiso  42828  sbiota1  43179  19.41rg  43297  ee223  43381  or2expropbilem1  45729  funressnfv  45740  fcoresf1  45766  2reuimp  45810  f1oresf1o2  45986  zm1nn  45997  nltle2tri  46008  el1fzopredsuc  46020  fzoopth  46022  elsetpreimafvssdm  46041  imasetpreimafvbijlemf1  46059  iccpartlt  46079  iccpartgt  46082  iccelpart  46088  icceuelpart  46091  iccpartnel  46093  fargshiftfo  46097  fargshiftfva  46098  lswn0  46099  ich2exprop  46126  prsprel  46142  sprsymrelfolem2  46148  sprsymrelfo  46152  poprelb  46179  reuopreuprim  46181  goldbachthlem2  46201  odz2prm2pw  46218  fmtnoprmfac1  46220  fmtnofac2lem  46223  prmdvdsfmtnof1lem2  46240  2pwp1prm  46244  sfprmdvdsmersenne  46258  lighneallem3  46262  requad01  46276  requad2  46278  even3prm2  46374  fppr2odd  46386  fpprwpprb  46395  gbegt5  46416  sbgoldbwt  46432  sbgoldbalt  46436  sbgoldbm  46439  bgoldbtbndlem2  46461  bgoldbtbndlem3  46462  bgoldbtbndlem4  46463  bgoldbtbnd  46464  tgblthelfgott  46470  tgoldbach  46472  isomuspgrlem2b  46484  isomuspgrlem2d  46486  isomuspgr  46489  isomgrsym  46491  upgrwlkupwlk  46505  lmod0rng  46629  rnglidlmcl  46733  rngqiprngimfo  46767  nzerooringczr  46924  ztprmneprm  46977  ply1mulgsumlem1  47021  ply1mulgsumlem2  47022  lcoel0  47063  linindslinci  47083  lindslinindimp2lem4  47096  lindslinindsimp2lem5  47097  snlindsntor  47106  ldepspr  47108  lincresunit2  47113  fllog2  47208  dignn0ldlem  47242  dignn0flhalflem1  47255  nn0sumshdiglemA  47259  nn0sumshdiglemB  47260  itcovalt2  47317  resum2sqorgt0  47349  eenglngeehlnmlem2  47378  rrx2linest  47382  itscnhlc0xyqsol  47405  itsclc0  47411  setrec1lem2  47687  aacllem  47802