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  841  dedlem0b  1041  sbequ1  2243  moexexlem  2628  ralrimdvva  3117  ceqsalt  3452  vtoclgft  3482  sbciegft  3749  reupick  4249  reusv3  5323  sbcop1  5396  propeqop  5415  pwssun  5476  wefrc  5574  ssrel  5683  ssrel2  5685  ssrelrel  5695  ssrelrn  5792  tz7.7  6277  ordtr2  6295  onmindif  6340  unizlim  6368  funssres  6462  f1ssf1  6731  fvmptt  6877  fveqdmss  6938  fvcofneq  6951  funsndifnop  7005  funfvima2  7089  isoini  7189  isopolem  7196  weniso  7205  f1ocnv2d  7500  limsssuc  7672  tfindsg  7682  limomss  7692  findsg  7720  funcnvuni  7752  f1oweALT  7788  funelss  7861  bropopvvv  7901  bropfvvvvlem  7902  bropfvvvv  7903  f1o2ndf1  7934  frxp  7938  suppfnss  7976  wfrlem12OLD  8122  onfununi  8143  tz7.49  8246  omordi  8359  omlimcl  8371  omass  8373  oeordsuc  8387  nnmordi  8424  nnmord  8425  omabs  8441  xpdom2  8807  infensuc  8891  findcard2  8909  findcard2d  8911  findcard2OLD  8986  findcard3  8987  frfi  8989  xpfi  9015  fsuppres  9083  dffi2  9112  elfiun  9119  ordiso2  9204  ordtypelem7  9213  suc11reg  9307  inf3lem2  9317  noinfep  9348  cantnfle  9359  cantnflem1  9377  cantnf  9381  trpredrec  9415  trcl  9417  epfrs  9420  frr3g  9445  r1sdom  9463  updjud  9623  pr2ne  9692  dfac8alem  9716  indcardi  9728  alephordi  9761  dfac12lem3  9832  pwsdompw  9891  cofsmo  9956  cfcoflem  9959  coftr  9960  isf32lem2  10041  isf32lem9  10048  axcc3  10125  domtriomlem  10129  axdc3lem2  10138  axdc3lem4  10140  zorn2lem4  10186  zorn2lem6  10188  zorn2lem7  10189  ttukeylem6  10201  uniimadom  10231  konigthlem  10255  fpwwe2lem7  10324  tskord  10467  tskcard  10468  grupr  10484  gruiin  10497  grudomon  10504  grur1a  10506  genpn0  10690  genpcd  10693  distrlem5pr  10714  psslinpr  10718  ltaddpr  10721  ltexprlem3  10725  ltexprlem6  10728  ltapr  10732  prlem936  10734  suplem1pr  10739  axpre-sup  10856  1re  10906  dedekindle  11069  lemul12a  11763  divgt0  11773  divge0  11774  lbreu  11855  sup2  11861  bndndx  12162  elnnz  12259  nzadd  12298  fzind  12348  fnn0ind  12349  uzwo  12580  lbzbi  12605  zmax  12614  zbtwnre  12615  irradd  12642  irrmul  12643  ledivge1le  12730  xrub  12975  supxrunb2  12983  infmremnf  13006  iccid  13053  uzsubsubfz  13207  fzrevral  13270  elfz0fzfz0  13290  fz0fzelfz0  13291  elfzmlbp  13296  elincfzoext  13373  ssfzoulel  13409  ssfzo12bi  13410  elfzonelfzo  13417  elfznelfzo  13420  elfznelfzob  13421  injresinjlem  13435  fleqceilz  13502  modaddmodup  13582  uzindi  13630  suppssfz  13642  mptnn0fsuppr  13647  le2sq2  13782  sqlecan  13853  facdiv  13929  facwordi  13931  faclbnd  13932  hashimarni  14084  hash2prd  14117  hashle2pr  14119  pr2pwpr  14121  fundmge2nop0  14134  fi1uzind  14139  brfi1indALT  14142  swrdnd2  14296  swrdnnn0nd  14297  swrdnd0  14298  pfxnd0  14329  swrdswrdlem  14345  swrdswrd  14346  ccatopth2  14358  wrd2ind  14364  pfxccatin12lem2a  14368  swrdccatin2  14370  pfxccatin12lem2  14372  pfxccatin12lem3  14373  swrdccat  14376  swrdccat3blem  14380  reuccatpfxs1lem  14387  repswswrd  14425  cshwidxmod  14444  cshwidx0  14447  2cshwcshw  14466  cshwcsh2id  14469  cau3lem  14994  caubnd  14998  climrlim2  15184  rlimcn3  15227  mulcn2  15233  climcau  15310  climbdd  15311  caucvg  15318  modfsummod  15434  p1modz1  15898  dvdsle  15947  dvdsdivcl  15953  ltoddhalfle  15998  halfleoddlt  15999  ndvdssub  16046  gcdcllem1  16134  dvdslegcd  16139  bezoutlem4  16178  dfgcd2  16182  lcmf  16266  lcmfunsnlem1  16270  lcmfunsnlem2lem1  16271  lcmfunsnlem  16274  lcmfdvdsb  16276  lcmfun  16278  coprmdvds1  16285  divgcdcoprm0  16298  cncongr1  16300  cncongr2  16301  prmfac1  16354  pcqcl  16485  dvdsprmpweqle  16515  oddprmdvds  16532  prmpwdvds  16533  infpnlem1  16539  prmgaplem5  16684  prmgaplem6  16685  prmgaplem7  16686  cshwshashlem1  16725  cictr  17434  initoeu2lem1  17645  initoeu2  17647  clatleglb  18151  lidrididd  18269  mulgaddcom  18642  mulginvcom  18643  cycsubm  18736  cyccom  18737  gsmsymgreqlem2  18954  symggen  18993  psgnunilem4  19020  sylow2blem3  19142  frgpnabllem1  19389  dprddisj2  19557  f1rhm0to0ALT  19900  lmodfopnelem1  20074  lssssr  20130  lss1d  20140  lspsncv0  20323  znrrg  20685  mplcoe5lem  21150  cply1mul  21375  coe1fzgsumdlem  21382  gsummoncoe1  21385  evl1gsumdlem  21432  mamufacex  21448  dmatelnd  21553  scmataddcl  21573  scmatsubcl  21574  scmatmulcl  21575  smatvscl  21581  mavmulsolcl  21608  mdetdiagid  21657  cramerlem3  21746  pmatcoe1fsupp  21758  cpmatacl  21773  cpmatmcllem  21775  mp2pm2mplem4  21866  chpscmat  21899  chfacfisf  21911  chfacfisfcpmat  21912  uniopn  21954  opnnei  22179  neindisj2  22182  restcls  22240  restntr  22241  tgcnp  22312  subbascn  22313  iscnp4  22322  lpcls  22423  cmpsublem  22458  cmpsub  22459  tgcmp  22460  cmpcld  22461  dfconn2  22478  1stcrest  22512  2ndcdisj  22515  1stccnp  22521  comppfsc  22591  kgencn2  22616  txlm  22707  kqreglem1  22800  filin  22913  isfil2  22915  ufilmax  22966  ufileu  22978  filufint  22979  cfinufil  22987  elfm2  23007  rnelfmlem  23011  rnelfm  23012  flimopn  23034  fbflim2  23036  flffbas  23054  fclsnei  23078  flimfnfcls  23087  fclscmp  23089  fcfnei  23094  cnpfcf  23100  alexsubALTlem2  23107  alexsubALTlem3  23108  alexsubALTlem4  23109  alexsubALT  23110  ptcmplem4  23114  qustgplem  23180  tsmsres  23203  tsmsxp  23214  metss  23570  metcnp3  23602  ovoliunnul  24576  ovolicc2lem3  24588  dyadmax  24667  itg2le  24809  bddiblnc  24911  itgcn  24914  ellimc3  24948  lhop1  25083  dvfsumrlim  25100  fta1g  25237  fta1  25373  aalioulem3  25399  aalioulem4  25400  ulmcaulem  25458  ulmcau  25459  logbgcd1irr  25849  xrlimcnp  26023  cxploglim  26032  jensen  26043  lgsqrmodndvds  26406  gausslemma2dlem1a  26418  gausslemma2dlem2  26420  gausslemma2dlem3  26421  lgsquad2lem2  26438  2lgslem1a1  26442  2sqlem6  26476  2sq2  26486  2sqnn  26492  2sqreultblem  26501  brbtwn2  27176  ax5seglem5  27204  axcontlem4  27238  axcontlem10  27244  umgrnloopv  27379  umgrnloop  27381  upgredgpr  27415  numedglnl  27417  usgrausgrb  27442  usgrnloopvALT  27471  usgrnloopALT  27473  usgredg2vlem2  27496  ushgredgedg  27499  ushgredgedgloop  27501  upgrreslem  27574  umgrreslem  27575  nbgr0vtxlem  27625  nbusgrvtxm1  27649  uvtxnbgrvtx  27663  cusgredg  27694  cusgrres  27718  cusgrsize2inds  27723  cusgrfi  27728  fusgrregdegfi  27839  ewlkle  27875  uspgr2wlkeqi  27917  wlklenvclwlkOLD  27925  lfgrwlkprop  27957  lfgrwlknloop  27959  pthdivtx  27998  2pthnloop  28000  upgrwlkdvdelem  28005  upgrspthswlk  28007  usgr2wlkneq  28025  usgr2trlncl  28029  usgr2pthlem  28032  usgr2pth  28033  uspgrn2crct  28074  crctcshwlkn0lem4  28079  crctcshwlkn0lem5  28080  crctcshwlkn0  28087  wlkiswwlks1  28133  wlkiswwlks2  28141  wlkiswwlksupgr2  28143  wwlksnred  28158  wwlksnext  28159  wwlksnextbi  28160  wwlksnextwrd  28163  wwlksnextinj  28165  wwlksnextproplem2  28176  wwlksnextproplem3  28177  wspthsnonn0vne  28183  wspn0  28190  2pthon3v  28209  umgrwwlks2on  28223  elwspths2on  28226  wpthswwlks2on  28227  clwwlk1loop  28253  clwwlkccatlem  28254  umgrclwwlkge2  28256  clwlkclwwlklem2a4  28262  clwlkclwwlklem2a  28263  clwlkclwwlklem3  28266  clwlkclwwlkf1lem3  28271  clwlkclwwlkfo  28274  clwwisshclwwslemlem  28278  erclwwlkeqlen  28284  erclwwlksym  28286  clwwlkf  28312  clwwlknscsh  28327  erclwwlknsym  28335  clwwlknonex2lem2  28373  clwwlknonex2  28374  upgr3v3e3cycl  28445  upgr4cycl4dv4e  28450  eucrctshift  28508  3vfriswmgr  28543  1to2vfriswmgr  28544  1to3vfriswmgr  28545  n4cyclfrgr  28556  4cyclusnfrgr  28557  frgrnbnb  28558  frgrncvvdeqlem8  28571  frgrwopreg  28588  frgr2wwlk1  28594  frgr2wwlkeqm  28596  2clwwlk2clwwlklem  28611  numclwwlk1lem2fo  28623  wlkl0  28632  numclwlk2lem2f  28642  frgrreggt1  28658  frgrreg  28659  frgrregord013  28660  frgrregord13  28661  frgrogt3nreg  28662  eulplig  28748  nmoub3i  29036  ipasslem5  29098  htthlem  29180  ocin  29559  spansneleq  29833  spansnss  29834  elspansn4  29836  h1datomi  29844  nmopub2tALT  30172  nmfnleub2  30189  hstel2  30482  cvnbtwn  30549  spansncv2  30556  dmdmd  30563  dmdbr3  30568  dmdbr4  30569  dmdbr5  30571  mdsl0  30573  mdexchi  30598  cvexchlem  30631  atcv1  30643  atomli  30645  atcvatlem  30648  atcvat2i  30650  chirredi  30657  mdsymlem3  30668  mdsymlem4  30669  sumdmdii  30678  sumdmdlem  30681  cdj1i  30696  ssrelf  30856  f1o3d  30863  fisshasheq  32973  umgr2cycllem  33002  cvxpconn  33104  satfv0  33220  satfsschain  33226  satfrel  33229  satfdm  33231  satfv0fun  33233  sat1el2xp  33241  gonarlem  33256  goalrlem  33258  satffunlem1lem1  33264  satffunlem2lem1  33266  satffunlem2lem2  33268  satffun  33271  mrsubccat  33380  msubvrs  33422  fundmpss  33646  dfon2lem6  33670  dfon2lem8  33672  dfon2lem9  33673  dfon2  33674  ttrclss  33706  soseq  33730  wzel  33745  nosepdmlem  33813  nodenselem8  33821  madebdaylemlrcut  34006  colinearxfr  34304  btwnconn1lem11  34326  lineintmo  34386  trer  34432  elicc3  34433  finminlem  34434  nn0prpwlem  34438  fnessref  34473  neibastop2  34477  fgmin  34486  tailfb  34493  ordcmp  34563  ee7.2aOLD  34577  bj-cbvalimt  34747  bj-ceqsalt0  34996  bj-ceqsalt1  34997  isbasisrelowllem1  35453  isbasisrelowllem2  35454  relowlpssretop  35462  fvineqsneu  35509  fvineqsneq  35510  wl-mo3t  35658  finixpnum  35689  matunitlindflem1  35700  matunitlindflem2  35701  poimirlem26  35730  poimirlem27  35731  poimirlem29  35733  ftc1anc  35785  fdc  35830  heibor1lem  35894  ghomco  35976  rngoueqz  36025  unichnidl  36116  dmncan1  36161  ax12indn  36884  lshpdisj  36928  lub0N  37130  glb0N  37134  leat2  37235  hlrelat2  37344  cvrexchlem  37360  cvratlem  37362  atcvrj0  37369  cvrat2  37370  snatpsubN  37691  linepsubN  37693  pmaple  37702  pmapsub  37709  elpaddn0  37741  paddasslem5  37765  trlval2  38104  cdlemn11pre  39151  dihord2pre  39166  mapdordlem2  39578  fsuppind  40202  sn-sup2  40360  pell1qrgap  40612  dford3lem1  40764  hbtlem5  40869  ntrneiiso  41590  sbiota1  41941  19.41rg  42059  ee223  42143  or2expropbilem1  44413  funressnfv  44424  fcoresf1  44450  2reuimp  44494  f1oresf1o2  44670  zm1nn  44682  nltle2tri  44693  el1fzopredsuc  44705  fzoopth  44707  elsetpreimafvssdm  44726  imasetpreimafvbijlemf1  44744  iccpartlt  44764  iccpartgt  44767  iccelpart  44773  icceuelpart  44776  iccpartnel  44778  fargshiftfo  44782  fargshiftfva  44783  lswn0  44784  ich2exprop  44811  prsprel  44827  sprsymrelfolem2  44833  sprsymrelfo  44837  poprelb  44864  reuopreuprim  44866  goldbachthlem2  44886  odz2prm2pw  44903  fmtnoprmfac1  44905  fmtnofac2lem  44908  prmdvdsfmtnof1lem2  44925  2pwp1prm  44929  sfprmdvdsmersenne  44943  lighneallem3  44947  requad01  44961  requad2  44963  even3prm2  45059  fppr2odd  45071  fpprwpprb  45080  gbegt5  45101  sbgoldbwt  45117  sbgoldbalt  45121  sbgoldbm  45124  bgoldbtbndlem2  45146  bgoldbtbndlem3  45147  bgoldbtbndlem4  45148  bgoldbtbnd  45149  tgblthelfgott  45155  tgoldbach  45157  isomuspgrlem2b  45169  isomuspgrlem2d  45171  isomuspgr  45174  isomgrsym  45176  upgrwlkupwlk  45190  lmod0rng  45314  nzerooringczr  45518  ztprmneprm  45571  ply1mulgsumlem1  45615  ply1mulgsumlem2  45616  lcoel0  45657  linindslinci  45677  lindslinindimp2lem4  45690  lindslinindsimp2lem5  45691  snlindsntor  45700  ldepspr  45702  lincresunit2  45707  fllog2  45802  dignn0ldlem  45836  dignn0flhalflem1  45849  nn0sumshdiglemA  45853  nn0sumshdiglemB  45854  itcovalt2  45911  resum2sqorgt0  45943  eenglngeehlnmlem2  45972  rrx2linest  45976  itscnhlc0xyqsol  45999  itsclc0  46005  setrec1lem2  46280  aacllem  46391