Theorem com23 84

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 41	. 2 ⊢ (𝜒 → ((𝜒 → 𝜃) → 𝜃))
3	1, 2	syl9 75	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  85  com13  86  pm2.04  88  pm2.86d  105  expcomd  453  impancom  455  a2and  849  dedlem0b  992  3com23  1263  ad5ant13  1293  ad5ant14  1294  ad5ant15  1295  ad5ant134  1305  ad5ant135  1306  moexex  2529  ralrimdvva  2957  ceqsalt  3201  vtoclgft  3227  vtoclgftOLD  3228  reu6  3362  sbciegft  3433  reupick  3870  reusv3  4802  ralxfrd  4805  ralxfrd2  4810  propeqop  4895  pwssun  4944  wefrc  5032  ssrel  5130  ssrelOLD  5131  ssrel2  5133  ssrelrel  5143  ssrelrn  5237  predpo  5615  tz7.7  5666  ordtr2  5685  onmindif  5732  unizlim  5761  funssres  5844  fv3  6116  fvmptt  6208  fveqdmss  6262  fvcofneq  6275  funsndifnop  6321  fmptsnd  6340  funfvima2  6397  isoini  6488  isopolem  6495  weniso  6504  f1ocnv2d  6784  limsssuc  6942  tfindsg  6952  limomss  6962  findsg  6985  funcnvuni  7012  f1oweALT  7043  bropopvvv  7142  bropfvvvvlem  7143  bropfvvvv  7144  f1o2ndf1  7172  frxp  7174  suppfnss  7207  wfr3g  7300  wfrlem12  7313  onfununi  7325  tz7.49  7427  omordi  7533  omlimcl  7545  omass  7547  oeordsuc  7561  nnmordi  7598  nnmord  7599  omabs  7614  xpdom2  7940  infensuc  8023  findcard2  8085  findcard2d  8087  findcard3  8088  frfi  8090  xpfi  8116  fsuppres  8183  dffi2  8212  elfiun  8219  ordiso2  8303  ordtypelem7  8312  suc11reg  8399  inf3lem2  8409  noinfep  8440  cantnfle  8451  cantnflem1  8469  cantnf  8473  trcl  8487  epfrs  8490  r1sdom  8520  pr2ne  8711  dfac8alem  8735  indcardi  8747  alephordi  8780  dfac12lem3  8850  pwsdompw  8909  cofsmo  8974  cfcoflem  8977  coftr  8978  isf32lem2  9059  isf32lem9  9066  axcc3  9143  domtriomlem  9147  axdc3lem2  9156  axdc3lem4  9158  zorn2lem4  9204  zorn2lem6  9206  zorn2lem7  9207  ttukeylem6  9219  uniimadom  9245  konigthlem  9269  fpwwe2lem8  9338  tskord  9481  tskcard  9482  grupr  9498  gruiin  9511  grudomon  9518  grur1a  9520  nqereu  9630  genpn0  9704  genpcd  9707  distrlem5pr  9728  psslinpr  9732  ltaddpr  9735  ltexprlem3  9739  ltexprlem6  9742  ltapr  9746  prlem936  9748  suplem1pr  9753  axpre-sup  9869  1re  9918  ltletr  10008  dedekindle  10080  lemul12a  10760  divgt0  10770  divge0  10771  lbreu  10852  sup2  10858  bndndx  11168  elnnz  11264  nzadd  11302  fzind  11351  fnn0ind  11352  uzwo  11627  eqreznegel  11650  lbzbi  11652  zmax  11661  zbtwnre  11662  irradd  11688  irrmul  11689  ledivge1le  11777  xrltletr  11864  xnn0xaddcl  11940  xrub  12014  supxrunb2  12022  infmremnf  12044  iccid  12091  uzsubsubfz  12234  fzrevral  12294  elfz0fzfz0  12313  fz0fzelfz0  12314  elfzmlbp  12319  elincfzoext  12393  elfzodifsumelfzo  12401  ssfzoulel  12428  ssfzo12bi  12429  elfzonelfzo  12436  elfznelfzo  12439  elfznelfzob  12440  injresinjlem  12450  fleqceilz  12515  modaddmodup  12595  uzindi  12643  suppssfz  12656  mptnn0fsuppr  12661  le2sq2  12801  sqlecan  12833  facdiv  12936  facwordi  12938  faclbnd  12939  hashimarni  13086  hash2prd  13114  pr2pwpr  13116  fundmge2nop0  13129  fi1uzind  13134  brfi1indALT  13137  fi1uzindOLD  13140  brfi1indALTOLD  13143  swrdnd2  13285  swrdswrdlem  13311  swrdswrd  13312  ccatopth2  13323  wrd2ind  13329  reuccats1lem  13331  swrdccatin1  13334  swrdccatin12lem2a  13336  swrdccatin2  13338  swrdccatin12lem2  13340  swrdccatin12lem3  13341  swrdccat  13344  swrdccat3blem  13346  repswswrd  13382  cshwidxmod  13400  cshwidx0  13403  2cshwcshw  13422  cshwcsh2id  13425  cau3lem  13942  caubnd  13946  climrlim2  14126  rlimuni  14129  rlimcn2  14169  mulcn2  14174  rlimno1  14232  climcau  14249  climbdd  14250  caucvg  14257  modfsummod  14367  dvdsle  14870  dvdsdivcl  14876  ltoddhalfle  14923  halfleoddlt  14924  ndvdssub  14971  gcdcllem1  15059  dvdslegcd  15064  bezoutlem4  15097  dfgcd2  15101  lcmf  15184  lcmfunsnlem1  15188  lcmfunsnlem2lem1  15189  lcmfunsnlem2  15191  lcmfunsnlem  15192  lcmfdvdsb  15194  lcmfun  15196  coprmdvds1  15203  coprmdvds  15204  coprmdvdsOLD  15205  coprmdvds2  15206  divgcdcoprm0  15217  cncongr1  15219  cncongr2  15220  prmfac1  15269  pcqcl  15399  dvdsprmpweqle  15428  oddprmdvds  15445  prmpwdvds  15446  infpnlem1  15452  prmgaplem5  15597  prmgaplem6  15598  prmgaplem7  15599  cshwshashlem1  15640  cictr  16288  initoeu2lem1  16487  initoeu2  16489  clatleglb  16949  mulgaddcom  17387  mulginvcom  17388  gsmsymgrfixlem1  17670  gsmsymgreqlem2  17674  symggen  17713  psgnunilem4  17740  sylow2blem3  17860  lsmdisj2  17918  frgpnabllem1  18099  dprddisj2  18261  f1rhm0to0ALT  18564  lmodfopnelem1  18722  lssssr  18774  lss1d  18784  lspsncv0  18967  mplcoe5lem  19288  cply1mul  19485  coe1fzgsumdlem  19492  gsummoncoe1  19495  evl1gsumdlem  19541  znrrg  19733  mamufacex  20014  dmatelnd  20121  scmataddcl  20141  scmatsubcl  20142  scmatmulcl  20143  smatvscl  20149  mavmulsolcl  20176  mdetdiagid  20225  cramerlem3  20314  pmatcoe1fsupp  20325  cpmatacl  20340  cpmatmcllem  20342  mp2pm2mplem4  20433  chpscmat  20466  chfacfisf  20478  chfacfisfcpmat  20479  uniopn  20527  opnnei  20734  neindisj2  20737  restcls  20795  restntr  20796  tgcnp  20867  subbascn  20868  iscnp4  20877  lmcnp  20918  lpcls  20978  cmpsublem  21012  cmpsub  21013  tgcmp  21014  cmpcld  21015  dfcon2  21032  1stcrest  21066  2ndcdisj  21069  1stccnp  21075  comppfsc  21145  kgencn2  21170  txlm  21261  kqreglem1  21354  filin  21468  isfil2  21470  fgss2  21488  fgfil  21489  ufilmax  21521  ufileu  21533  filufint  21534  cfinufil  21542  elfm2  21562  rnelfmlem  21566  rnelfm  21567  fmfnfmlem2  21569  fmfnfmlem4  21571  flimopn  21589  fbflim2  21591  flffbas  21609  fclsnei  21633  flimfnfcls  21642  fclscmp  21644  ufilcmp  21646  fcfnei  21649  cnpfcf  21655  alexsubALTlem2  21662  alexsubALTlem3  21663  alexsubALTlem4  21664  alexsubALT  21665  ptcmplem4  21669  qustgplem  21734  tsmsres  21757  tsmsxp  21768  metss  22123  metcnp3  22155  ivthlem2  23028  ivthlem3  23029  ovoliunnul  23082  ovolicc2lem3  23094  dyadmax  23172  itg2le  23312  itgcn  23415  ellimc3  23449  lhop1  23581  dvfsumrlim  23598  fta1g  23731  fta1  23867  aalioulem3  23893  aalioulem4  23894  ulmcaulem  23952  ulmcau  23953  xrlimcnp  24495  cxploglim  24504  jensen  24515  lgsqrmodndvds  24878  gausslemma2dlem1a  24890  gausslemma2dlem2  24892  gausslemma2dlem3  24893  lgsquad2lem2  24910  2lgslem1a1  24914  2sqlem6  24948  brbtwn2  25585  ax5seglem5  25613  axcontlem4  25647  axcontlem10  25653  umgrnloopv  25772  umgrnloop  25774  umgrislfupgrlem  25788  upgredgpr  25815  usgranloopv  25907  usgranloop  25908  usgra2edg  25911  usgraedg4  25916  usgra1v  25919  usgraidx2vlem2  25921  usgrafisindb0  25937  usgrafisindb1  25938  usgrares1  25939  cusgrarn  25988  cusgrares  26001  cusgrasize2inds  26005  cusgrafi  26010  sizeusglecusg  26014  usgrwlknloop  26093  1pthoncl  26122  wlkdvspthlem  26137  wlkdvspth  26138  usgra2wlkspthlem2  26148  cyclnspth  26159  fargshiftfo  26166  fargshiftfva  26167  usgrcyclnl1  26168  nvnencycllem  26171  constr3trllem2  26179  4cycl4dv  26195  wwlknimp  26215  wlkiswwlk2  26225  wwlknred  26251  wwlknext  26252  wwlknextbi  26253  wwlkextwrd  26256  wwlkextinj  26258  wwlkextproplem2  26270  wwlkextproplem3  26271  clwwlkgt0  26299  clwwlknprop  26300  clwlkisclwwlklem2a4  26312  clwlkisclwwlklem2a  26313  clwlkisclwwlklem0  26316  clwwlkf  26322  wwlkext2clwwlk  26331  clwwisshclwwlem1  26333  erclwwlkeqlen  26340  erclwwlksym  26342  clwwlknscsh  26347  erclwwlkneqlen  26352  erclwwlknsym  26354  wlklenvclwlk  26366  clwlkfclwwlk  26371  clwlkfoclwwlk  26372  el2wlkonot  26396  usg2wotspth  26411  usg2spthonot  26415  usg2spthonot0  26416  usgfiregdegfi  26438  nbhashuvtx1  26442  rusgraprop4  26471  eupatrl  26495  3vfriswmgra  26532  1to2vfriswmgra  26533  1to3vfriswmgra  26534  3cyclfrgrarn  26540  n4cyclfrgra  26545  4cyclusnfrgra  26546  frgranbnb  26547  frgrancvvdeqlemB  26565  frg2wot1  26584  frg2woteqm  26586  frg2woteq  26587  usg2spot2nb  26592  2spotmdisj  26595  usgreghash2spot  26596  frgregordn0  26597  numclwwlkovf2ex  26613  numclwlk1lem2fo  26622  numclwlk2lem2f  26630  numclwwlk8  26642  frgrareg  26644  frgraregord013  26645  frgraogt3nreg  26647  nmoub3i  27012  ipasslem5  27074  htthlem  27158  ocin  27539  spansneleq  27813  spansnss  27814  elspansn4  27816  h1datomi  27824  nmopub2tALT  28152  nmfnleub2  28169  hstel2  28462  cvnbtwn  28529  spansncv2  28536  dmdmd  28543  dmdbr3  28548  dmdbr4  28549  dmdbr5  28551  mdsl0  28553  mdexchi  28578  cvexchlem  28611  atcv1  28623  atomli  28625  atcvatlem  28628  atcvat2i  28630  chirredi  28637  mdsymlem3  28648  mdsymlem4  28649  sumdmdii  28658  sumdmdlem  28661  cdj1i  28676  ssrelf  28805  f1o3d  28813  cvxpcon  30478  mrsubccat  30669  msubvrs  30711  fundmpss  30910  dfon2lem6  30937  dfon2lem8  30939  dfon2lem9  30940  dfon2  30941  trpredrec  30982  soseq  30995  wzel  31015  wzelOLD  31016  frr3g  31023  frrlem11  31036  nodenselem5  31084  nodenselem7  31086  nodenselem8  31087  nofulllem5  31105  colinearxfr  31352  btwnconn1lem11  31374  lineintmo  31434  trer  31480  elicc3  31481  finminlem  31482  nn0prpwlem  31487  fnessref  31522  neibastop2  31526  fgmin  31535  tailfb  31542  ordcmp  31616  ee7.2aOLD  31630  bj-ceqsalt0  32067  bj-ceqsalt1  32068  isbasisrelowllem1  32379  isbasisrelowllem2  32380  relowlpssretop  32388  wl-mo3t  32537  finixpnum  32564  matunitlindflem1  32575  matunitlindflem2  32576  poimirlem26  32605  poimirlem27  32606  poimirlem29  32608  bddiblnc  32650  ftc1anc  32663  fdc  32711  heibor1lem  32778  ghomco  32860  rngoueqz  32909  unichnidl  33000  dmncan1  33045  ax12indn  33246  lshpdisj  33292  lub0N  33494  glb0N  33498  leat2  33599  hlrelat2  33707  cvrexchlem  33723  cvratlem  33725  atcvrj0  33732  cvrat2  33733  snatpsubN  34054  linepsubN  34056  pmaple  34065  pmapsub  34072  elpaddn0  34104  paddasslem5  34128  trlval2  34468  cdlemn11pre  35517  dihord2pre  35532  mapdordlem2  35944  pell1qrgap  36456  dford3lem1  36611  hbtlem5  36717  ntrneiiso  37409  sbiota1  37657  19.41rg  37787  ee223  37880  funressnfv  39857  nltle2tri  39942  el1fzopredsuc  39948  iccpartlt  39962  iccpartgt  39965  iccelpart  39971  icceuelpart  39974  iccpartnel  39976  goldbachthlem2  39996  odz2prm2pw  40013  fmtnoprmfac1  40015  fmtnofac2lem  40018  prmdvdsfmtnof1lem2  40035  2pwp1prm  40041  sfprmdvdsmersenne  40058  lighneallem3  40062  gbegt5  40183  bgoldbwt  40199  sgoldbalt  40203  bgoldbtbndlem2  40222  bgoldbtbndlem3  40223  bgoldbtbndlem4  40224  bgoldbtbnd  40225  tgblthelfgott  40229  tgoldbach  40232  tgblthelfgottOLD  40236  tgoldbachOLD  40239  lswn0  40242  pfxccatin12lem2  40287  reuccatpfxs1lem  40296  f1ssf1  40328  zm1nn  40348  fzoopth  40360  usgrausgrb  40399  usgrnloopvALT  40428  usgrnloopALT  40430  uhgr2edg  40435  usgredg2vlem2  40453  ushgredgedga  40456  ushgredgedgaloop  40458  nbgr0vtxlem  40577  nbusgrvtxm1  40607  uvtxanbgrvtx  40619  cusgredg  40646  cusgrres  40664  cusgrsize2inds  40669  cusgrfi  40674  fusgrregdegfi  40769  ewlkle  40807  upgrewlkle2  40808  upgr1wlkwlk  40847  upgrwlkedg  40850  uspgr2wlkeqi  40856  1wlkv0  40859  1wlklenvclwlk  40863  lfgrwlkprop  40896  lfgr1wlknloop  40898  pthdivtx  40935  2pthnloop  40937  upgrwlkdvdelem  40942  upgrspths1wlk  40944  usgr2wlkneq  40962  usgr2trlncl  40966  usgr2pthlem  40969  usgr2pth  40970  crctcsh1wlkn0lem4  41016  crctcsh1wlkn0lem5  41017  crctcsh1wlkn0  41024  1wlkiswwlks1  41064  1wlkiswwlks2  41072  1wlkiswwlksupgr2  41074  wwlksnred  41098  wwlksnext  41099  wwlksnextbi  41100  wwlksnextwrd  41103  wwlksnextinj  41105  wwlksnextproplem2  41116  wwlksnextproplem3  41117  wspthsnonn0vne  41124  2pthon3v-av  41150  wwlks2onv  41158  umgrwwlks2on  41161  elwspths2on  41163  wpthswwlks2on  41164  clwlkclwwlklem2a4  41206  clwlkclwwlklem2a  41207  clwlkclwwlklem3  41210  clwwlks1loop  41215  umgrclwwlksge2  41219  clwwlksf  41222  wwlksext2clwwlk  41231  clwwisshclwwslemlem  41233  erclwwlkseqlen  41240  erclwwlkssym  41242  clwwlksnscsh  41247  erclwwlksnsym  41254  clwlksfclwwlk  41269  upgr3v3e3cycl  41347  upgr4cycl4dv4e  41352  upgreupthi  41376  eucrctshift  41411  3vfriswmgr  41448  1to2vfriswmgr  41449  1to3vfriswmgr  41450  n4cyclfrgr  41461  4cyclusnfrgr  41462  frgrnbnb  41463  frgrncvvdeqlemB  41477  frgr2wwlk1  41494  fusgr2wsp2nb  41498  2wspmdisj  41501  fusgreghash2wsp  41502  frrusgrord0  41503  av-clwwlkextfrlem1  41509  av-extwwlkfablem2  41510  av-numclwwlkovf2ex  41517  av-numclwlk1lem2fo  41525  av-numclwlk2lem2f  41533  av-numclwwlk8  41546  av-frgrareggt1  41547  av-frgrareg  41548  av-frgraregord013  41549  av-frgraregord13  41550  av-frgraogt3nreg  41551  lmod0rng  41658  nzerooringczr  41864  ztprmneprm  41918  ply1mulgsumlem1  41968  ply1mulgsumlem2  41969  lcoel0  42011  linindslinci  42031  lindslinindimp2lem4  42044  lindslinindsimp2lem5  42045  snlindsntor  42054  ldepspr  42056  lincresunit2  42061  fllog2  42160  dignn0ldlem  42194  dignn0flhalflem1  42207  nn0sumshdiglemA  42211  nn0sumshdiglemB  42212  setrec1lem2  42234  aacllem  42356