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  expcomd  404  impancom  441  ad5ant13OLD  759  ad5ant14OLD  761  ad5ant15OLD  763  a2and  862  dedlem0b  1058  3com23OLD  1442  ad5ant134OLD  1476  ad5ant135OLD  1478  moexex  2716  ralrimdvva  3173  ceqsalt  3433  vtoclgft  3459  reu6  3604  sbciegft  3675  reupick  4123  reusv3  5087  ralxfrd  5090  ralxfrd2  5094  propeqop  5175  pwssun  5228  wefrc  5318  ssrel  5423  ssrelOLD  5424  ssrel2  5426  ssrelrel  5436  ssrelrn  5530  predpo  5925  tz7.7  5976  ordtr2  5994  onmindif  6040  unizlim  6067  funssres  6154  f1ssf1  6394  fv3  6436  fvmptt  6531  fveqdmss  6586  fvcofneq  6599  funsndifnop  6650  fmptsnd  6670  funfvima2  6728  isoini  6822  isopolem  6829  weniso  6838  f1ocnv2d  7126  limsssuc  7290  tfindsg  7300  limomss  7310  findsg  7333  funcnvuni  7359  f1oweALT  7392  bropopvvv  7499  bropfvvvvlem  7500  bropfvvvv  7501  f1o2ndf1  7529  frxp  7531  suppfnss  7564  suppfnssOLD  7565  wfr3g  7658  wfrlem12  7672  onfununi  7684  tz7.49  7786  omordi  7893  omlimcl  7905  omass  7907  oeordsuc  7921  nnmordi  7958  nnmord  7959  omabs  7974  xpdom2  8304  infensuc  8387  findcard2  8449  findcard2d  8451  findcard3  8452  frfi  8454  xpfi  8480  fsuppres  8549  dffi2  8578  elfiun  8585  ordiso2  8669  ordtypelem7  8678  suc11reg  8773  inf3lem2  8783  noinfep  8814  cantnfle  8825  cantnflem1  8843  cantnf  8847  trcl  8861  epfrs  8864  r1sdom  8894  updjud  9053  pr2ne  9121  dfac8alem  9145  indcardi  9157  alephordi  9190  dfac12lem3  9262  pwsdompw  9321  cofsmo  9386  cfcoflem  9389  coftr  9390  isf32lem2  9471  isf32lem9  9478  axcc3  9555  domtriomlem  9559  axdc3lem2  9568  axdc3lem4  9570  zorn2lem4  9616  zorn2lem6  9618  zorn2lem7  9619  ttukeylem6  9631  uniimadom  9661  konigthlem  9685  fpwwe2lem8  9754  tskord  9897  tskcard  9898  grupr  9914  gruiin  9927  grudomon  9934  grur1a  9936  nqereu  10046  genpn0  10120  genpcd  10123  distrlem5pr  10144  psslinpr  10148  ltaddpr  10151  ltexprlem3  10155  ltexprlem6  10158  ltapr  10162  prlem936  10164  suplem1pr  10169  axpre-sup  10285  1re  10335  ltletr  10424  dedekindle  10496  lemul12a  11176  divgt0  11186  divge0  11187  lbreu  11268  sup2  11274  bndndx  11578  elnnz  11673  nzadd  11711  fzind  11761  fnn0ind  11762  uzwo  11990  eqreznegel  12013  lbzbi  12015  zmax  12024  zbtwnre  12025  irradd  12051  irrmul  12052  ledivge1le  12135  xrltletr  12226  xnn0xaddcl  12304  xrub  12380  supxrunb2  12388  infmremnf  12411  iccid  12458  uzsubsubfz  12606  fzrevral  12668  elfz0fzfz0  12688  fz0fzelfz0  12689  elfzmlbp  12694  elincfzoext  12770  elfzodifsumelfzo  12778  ssfzoulel  12806  ssfzo12bi  12807  elfzonelfzo  12814  elfznelfzo  12817  elfznelfzob  12818  injresinjlem  12832  fleqceilz  12897  modaddmodup  12977  uzindi  13025  suppssfz  13037  mptnn0fsuppr  13042  le2sq2  13182  sqlecan  13214  facdiv  13314  facwordi  13316  faclbnd  13317  hashimarni  13465  hash2prd  13494  hashle2pr  13496  pr2pwpr  13498  fundmge2nop0  13511  fi1uzind  13516  brfi1indALT  13519  swrdnd2  13677  swrdswrdlem  13703  swrdswrd  13704  ccatopth2  13715  wrd2ind  13721  reuccats1lem  13723  swrdccatin1  13727  swrdccatin12lem2a  13729  swrdccatin2  13731  swrdccatin12lem2  13733  swrdccatin12lem3  13734  swrdccat  13737  swrdccat3blem  13739  repswswrd  13775  cshwidxmod  13793  cshwidx0  13796  2cshwcshw  13815  cshwcsh2id  13818  cau3lem  14337  caubnd  14341  climrlim2  14521  rlimuni  14524  rlimcn2  14564  mulcn2  14569  rlimno1  14627  climcau  14644  climbdd  14645  caucvg  14652  modfsummod  14768  p1modz1  15230  dvdsle  15275  dvdsdivcl  15281  ltoddhalfle  15325  halfleoddlt  15326  ndvdssub  15372  gcdcllem1  15460  dvdslegcd  15465  bezoutlem4  15498  dfgcd2  15502  lcmf  15585  lcmfunsnlem1  15589  lcmfunsnlem2lem1  15590  lcmfunsnlem2  15592  lcmfunsnlem  15593  lcmfdvdsb  15595  lcmfun  15597  coprmdvds1  15604  coprmdvds  15605  coprmdvds2  15606  divgcdcoprm0  15617  cncongr1  15619  cncongr2  15620  prmfac1  15668  pcqcl  15798  dvdsprmpweqle  15827  oddprmdvds  15844  prmpwdvds  15845  infpnlem1  15851  prmgaplem5  15996  prmgaplem6  15997  prmgaplem7  15998  cshwshashlem1  16034  cictr  16689  initoeu2lem1  16888  initoeu2  16890  clatleglb  17351  mulgaddcom  17788  mulginvcom  17789  gsmsymgrfixlem1  18068  gsmsymgreqlem2  18072  symggen  18111  psgnunilem4  18138  sylow2blem3  18258  lsmdisj2  18316  frgpnabllem1  18497  dprddisj2  18660  f1rhm0to0ALT  18965  lmodfopnelem1  19123  lssssr  19179  lssssrOLD  19180  lss1d  19190  lspsncv0  19374  lspsncv0OLD  19375  mplcoe5lem  19696  cply1mul  19892  coe1fzgsumdlem  19899  gsummoncoe1  19902  evl1gsumdlem  19948  znrrg  20141  mamufacex  20426  dmatelnd  20534  scmataddcl  20554  scmatsubcl  20555  scmatmulcl  20556  smatvscl  20562  mavmulsolcl  20589  mdetdiagid  20638  cramerlem3  20729  pmatcoe1fsupp  20740  cpmatacl  20755  cpmatmcllem  20757  mp2pm2mplem4  20848  chpscmat  20881  chfacfisf  20893  chfacfisfcpmat  20894  uniopn  20936  opnnei  21159  neindisj2  21162  restcls  21220  restntr  21221  tgcnp  21292  subbascn  21293  iscnp4  21302  lmcnp  21343  lpcls  21403  cmpsublem  21437  cmpsub  21438  tgcmp  21439  cmpcld  21440  dfconn2  21457  1stcrest  21491  2ndcdisj  21494  1stccnp  21500  comppfsc  21570  kgencn2  21595  txlm  21686  kqreglem1  21779  filin  21892  isfil2  21894  fgss2  21912  fgfil  21913  ufilmax  21945  ufileu  21957  filufint  21958  cfinufil  21966  elfm2  21986  rnelfmlem  21990  rnelfm  21991  fmfnfmlem2  21993  fmfnfmlem4  21995  flimopn  22013  fbflim2  22015  flffbas  22033  fclsnei  22057  flimfnfcls  22066  fclscmp  22068  ufilcmp  22070  fcfnei  22073  cnpfcf  22079  alexsubALTlem2  22086  alexsubALTlem3  22087  alexsubALTlem4  22088  alexsubALT  22089  ptcmplem4  22093  qustgplem  22158  tsmsres  22181  tsmsxp  22192  metss  22547  metcnp3  22579  ivthlem2  23456  ivthlem3  23457  ovoliunnul  23511  ovolicc2lem3  23523  dyadmax  23602  itg2le  23743  itgcn  23846  ellimc3  23880  lhop1  24014  dvfsumrlim  24031  fta1g  24164  fta1  24300  aalioulem3  24326  aalioulem4  24327  ulmcaulem  24385  ulmcau  24386  xrlimcnp  24932  cxploglim  24941  jensen  24952  lgsqrmodndvds  25315  gausslemma2dlem1a  25327  gausslemma2dlem2  25329  gausslemma2dlem3  25330  lgsquad2lem2  25347  2lgslem1a1  25351  2sqlem6  25385  brbtwn2  26022  ax5seglem5  26050  axcontlem4  26084  axcontlem10  26090  umgrnloopv  26238  umgrnloop  26240  umgrislfupgrlem  26254  upgredgpr  26275  numedglnl  26277  usgrausgrb  26302  usgrnloopvALT  26331  usgrnloopALT  26333  uhgr2edg  26338  usgredg2vlem2  26356  ushgredgedg  26359  ushgredgedgloop  26361  ushgredgedgloopOLD  26362  upgrreslem  26435  umgrreslem  26436  nbgr0vtxlem  26490  nbusgrvtxm1  26520  uvtxnbgrvtx  26536  cusgredg  26571  cusgrres  26595  cusgrsize2inds  26600  cusgrfi  26605  fusgrregdegfi  26716  ewlkle  26752  upgrewlkle2  26753  uspgr2wlkeqi  26795  wlkv0  26798  wlklenvclwlk  26802  lfgrwlkprop  26835  lfgrwlknloop  26837  pthdivtx  26876  2pthnloop  26878  upgrwlkdvdelem  26883  upgrspthswlk  26885  usgr2wlkneq  26903  usgr2trlncl  26907  usgr2pthlem  26910  usgr2pth  26911  uspgrn2crct  26952  crctcshwlkn0lem4  26957  crctcshwlkn0lem5  26958  crctcshwlkn0  26965  wlkiswwlks1  27017  wlkiswwlks2  27025  wlkiswwlksupgr2  27027  wwlksnred  27052  wwlksnext  27053  wwlksnextbi  27054  wwlksnextwrd  27057  wwlksnextinj  27059  wwlksnextproplem2  27071  wwlksnextproplem3  27072  wspthsnonn0vne  27080  wspn0  27087  2pthon3v  27106  umgrwwlks2on  27121  elwspths2on  27124  wpthswwlks2on  27125  wpthswwlks2onOLD  27126  clwwlk1loop  27154  clwwlkccatlem  27155  umgrclwwlkge2  27157  clwlkclwwlklem2a4  27163  clwlkclwwlklem2a  27164  clwlkclwwlklem3  27167  clwlkclwwlkf1lem3  27172  clwlkclwwlkfo  27175  clwwisshclwwslemlem  27179  erclwwlkeqlen  27185  erclwwlksym  27187  clwwlkf  27219  wwlksext2clwwlkOLD  27231  clwwlknscsh  27236  erclwwlknsym  27244  clwlksfclwwlkOLD  27259  clwwlknonwwlknonbOLD  27298  clwwlknonex2lem2  27300  clwwlknonex2  27301  upgr3v3e3cycl  27376  upgr4cycl4dv4e  27381  eucrctshift  27439  3vfriswmgr  27476  1to2vfriswmgr  27477  1to3vfriswmgr  27478  n4cyclfrgr  27489  4cyclusnfrgr  27490  frgrnbnb  27491  frgrncvvdeqlem8  27504  frgrwopreg  27521  frgr2wwlk1  27527  frgr2wwlkeqm  27529  numclwwlk2lem1lemOLD  27542  2clwwlk2clwwlklem  27546  numclwwlk1lem2fo  27560  wlkl0  27570  numclwlk2lem2f  27580  numclwlk2lem2fOLD  27587  frgrreggt1  27604  frgrreg  27605  frgrregord013  27606  frgrregord13  27607  frgrogt3nreg  27608  eulplig  27691  nmoub3i  27979  ipasslem5  28041  htthlem  28125  ocin  28506  spansneleq  28780  spansnss  28781  elspansn4  28783  h1datomi  28791  nmopub2tALT  29119  nmfnleub2  29136  hstel2  29429  cvnbtwn  29496  spansncv2  29503  dmdmd  29510  dmdbr3  29515  dmdbr4  29516  dmdbr5  29518  mdsl0  29520  mdexchi  29545  cvexchlem  29578  atcv1  29590  atomli  29592  atcvatlem  29595  atcvat2i  29597  chirredi  29604  mdsymlem3  29615  mdsymlem4  29616  sumdmdii  29625  sumdmdlem  29628  cdj1i  29643  ssrelf  29775  f1o3d  29781  cvxpconn  31569  mrsubccat  31760  msubvrs  31802  fundmpss  32008  dfon2lem6  32035  dfon2lem8  32037  dfon2lem9  32038  dfon2  32039  trpredrec  32080  soseq  32097  wzel  32112  frr3g  32122  nosepdmlem  32176  nodenselem8  32184  colinearxfr  32525  btwnconn1lem11  32547  lineintmo  32607  trer  32653  elicc3  32654  finminlem  32655  nn0prpwlem  32660  fnessref  32695  neibastop2  32699  fgmin  32708  tailfb  32715  ordcmp  32785  ee7.2aOLD  32799  bj-ceqsalt0  33200  bj-ceqsalt1  33201  isbasisrelowllem1  33538  isbasisrelowllem2  33539  relowlpssretop  33547  wl-mo3t  33691  finixpnum  33726  matunitlindflem1  33737  matunitlindflem2  33738  poimirlem26  33767  poimirlem27  33768  poimirlem29  33770  bddiblnc  33811  ftc1anc  33824  fdc  33871  heibor1lem  33938  ghomco  34020  rngoueqz  34069  unichnidl  34160  dmncan1  34205  ax12indn  34741  lshpdisj  34786  lub0N  34988  glb0N  34992  leat2  35093  hlrelat2  35202  cvrexchlem  35218  cvratlem  35220  atcvrj0  35227  cvrat2  35228  snatpsubN  35549  linepsubN  35551  pmaple  35560  pmapsub  35567  elpaddn0  35599  paddasslem5  35623  trlval2  35962  cdlemn11pre  37009  dihord2pre  37024  mapdordlem2  37436  pell1qrgap  37958  dford3lem1  38112  hbtlem5  38217  ntrneiiso  38907  sbiota1  39152  19.41rg  39282  ee223  39375  funressnfv  41680  f1oresf1o2  41899  zm1nn  41910  nltle2tri  41916  el1fzopredsuc  41928  fzoopth  41930  iccpartlt  41953  iccpartgt  41956  iccelpart  41962  icceuelpart  41965  iccpartnel  41967  fargshiftfo  41971  fargshiftfva  41972  lswn0  41973  pfxccatin12lem2  42017  reuccatpfxs1lem  42026  goldbachthlem2  42051  odz2prm2pw  42068  fmtnoprmfac1  42070  fmtnofac2lem  42073  prmdvdsfmtnof1lem2  42090  2pwp1prm  42096  sfprmdvdsmersenne  42113  lighneallem3  42117  even3prm2  42221  gbegt5  42242  sbgoldbwt  42258  sbgoldbalt  42262  sbgoldbm  42265  bgoldbtbndlem2  42287  bgoldbtbndlem3  42288  bgoldbtbndlem4  42289  bgoldbtbnd  42290  tgblthelfgott  42296  tgoldbach  42298  upgrwlkupwlk  42307  prsprel  42323  sprsymrelfolem2  42329  sprsymrelfo  42333  lmod0rng  42454  nzerooringczr  42658  ztprmneprm  42711  ply1mulgsumlem1  42760  ply1mulgsumlem2  42761  lcoel0  42803  linindslinci  42823  lindslinindimp2lem4  42836  lindslinindsimp2lem5  42837  snlindsntor  42846  ldepspr  42848  lincresunit2  42853  fllog2  42948  dignn0ldlem  42982  dignn0flhalflem1  42995  nn0sumshdiglemA  42999  nn0sumshdiglemB  43000  setrec1lem2  43021  aacllem  43136