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  843  dedlem0b  1043  sbequ1  2240  moexexlem  2627  ralrimdvva  3201  ceqsalt  3473  vtoclgft  3507  sbciegft  3772  reupick  4273  reusv3  5355  sbcop1  5439  propeqop  5458  pwssun  5522  wefrc  5621  ssrel  5731  ssrelOLD  5732  ssrel2  5734  ssrelrel  5745  ssrelrn  5843  tz7.7  6336  ordtr2  6354  onmindif  6402  unizlim  6432  funssres  6537  f1ssf1  6808  fvmptt  6960  fveqdmss  7021  fvcofneq  7034  funsndifnop  7088  funfvima2  7172  isoini  7274  isopolem  7281  weniso  7290  f1ocnv2d  7593  limsssuc  7773  tfindsg  7784  limomss  7794  findsg  7823  funcnvuni  7855  f1oweALT  7892  funelss  7965  bropopvvv  8007  bropfvvvvlem  8008  bropfvvvv  8009  f1o2ndf1  8039  frxp  8043  soseq  8055  suppfnss  8084  wfrlem12OLD  8230  onfununi  8251  tz7.49  8355  omordi  8477  omlimcl  8489  omass  8491  oeordsuc  8505  nnmordi  8542  nnmord  8543  omabs  8561  xpdom2  8941  infensuc  9029  findcard2  9038  findcard2d  9040  findcard2OLD  9158  findcard3  9159  findcard3OLD  9160  frfi  9162  xpfiOLD  9192  fsuppres  9260  dffi2  9289  elfiun  9296  ordiso2  9381  ordtypelem7  9390  suc11reg  9485  inf3lem2  9495  noinfep  9526  cantnfle  9537  cantnflem1  9555  cantnf  9559  ttrclss  9586  trcl  9594  epfrs  9597  frr3g  9622  r1sdom  9640  updjud  9800  pr2neOLD  9871  dfac8alem  9895  indcardi  9907  alephordi  9940  dfac12lem3  10011  pwsdompw  10070  cofsmo  10135  cfcoflem  10138  coftr  10139  isf32lem2  10220  isf32lem9  10227  axcc3  10304  domtriomlem  10308  axdc3lem2  10317  axdc3lem4  10319  zorn2lem4  10365  zorn2lem6  10367  zorn2lem7  10368  ttukeylem6  10380  uniimadom  10410  konigthlem  10434  fpwwe2lem7  10503  tskord  10646  tskcard  10647  grupr  10663  gruiin  10676  grudomon  10683  grur1a  10685  genpn0  10869  genpcd  10872  distrlem5pr  10893  psslinpr  10897  ltaddpr  10900  ltexprlem3  10904  ltexprlem6  10907  ltapr  10911  prlem936  10913  suplem1pr  10918  axpre-sup  11035  1re  11085  dedekindle  11249  lemul12a  11943  divgt0  11953  divge0  11954  lbreu  12035  sup2  12041  bndndx  12342  elnnz  12439  nzadd  12478  fzind  12528  fnn0ind  12529  uzwo  12761  lbzbi  12786  zmax  12795  zbtwnre  12796  irradd  12823  irrmul  12824  ledivge1le  12911  xrub  13156  supxrunb2  13164  infmremnf  13187  iccid  13234  uzsubsubfz  13388  fzrevral  13451  elfz0fzfz0  13471  fz0fzelfz0  13472  elfzmlbp  13477  elincfzoext  13555  ssfzoulel  13591  ssfzo12bi  13592  elfzonelfzo  13599  elfznelfzo  13602  elfznelfzob  13603  injresinjlem  13617  fleqceilz  13684  modaddmodup  13764  uzindi  13812  suppssfz  13824  mptnn0fsuppr  13829  le2sq2  13964  sqlecan  14035  facdiv  14111  facwordi  14113  faclbnd  14114  hashimarni  14265  hash2prd  14298  hashle2pr  14300  pr2pwpr  14302  fundmge2nop0  14315  fi1uzind  14320  brfi1indALT  14323  swrdnd2  14471  swrdnnn0nd  14472  swrdnd0  14473  pfxnd0  14504  swrdswrdlem  14520  swrdswrd  14521  ccatopth2  14533  wrd2ind  14539  pfxccatin12lem2a  14543  swrdccatin2  14545  pfxccatin12lem2  14547  pfxccatin12lem3  14548  swrdccat  14551  swrdccat3blem  14555  reuccatpfxs1lem  14562  repswswrd  14600  cshwidxmod  14619  cshwidx0  14622  2cshwcshw  14642  cshwcsh2id  14645  cau3lem  15170  caubnd  15174  climrlim2  15360  rlimcn3  15403  mulcn2  15409  climcau  15486  climbdd  15487  caucvg  15494  modfsummod  15610  p1modz1  16074  dvdsle  16123  dvdsdivcl  16129  ltoddhalfle  16174  halfleoddlt  16175  ndvdssub  16222  gcdcllem1  16310  dvdslegcd  16315  bezoutlem4  16354  dfgcd2  16358  lcmf  16440  lcmfunsnlem1  16444  lcmfunsnlem2lem1  16445  lcmfunsnlem  16448  lcmfdvdsb  16450  lcmfun  16452  coprmdvds1  16459  divgcdcoprm0  16472  cncongr1  16474  cncongr2  16475  prmfac1  16528  pcqcl  16659  dvdsprmpweqle  16689  oddprmdvds  16706  prmpwdvds  16707  infpnlem1  16713  prmgaplem5  16858  prmgaplem6  16859  prmgaplem7  16860  cshwshashlem1  16899  cictr  17619  initoeu2lem1  17831  initoeu2  17833  clatleglb  18338  lidrididd  18456  mulgaddcom  18828  mulginvcom  18829  cycsubm  18922  cyccom  18923  gsmsymgreqlem2  19140  symggen  19179  psgnunilem4  19206  sylow2blem3  19328  frgpnabllem1  19574  dprddisj2  19741  f1rhm0to0ALT  20087  lmodfopnelem1  20269  lssssr  20325  lss1d  20335  lspsncv0  20518  znrrg  20883  mplcoe5lem  21350  cply1mul  21575  coe1fzgsumdlem  21582  gsummoncoe1  21585  evl1gsumdlem  21632  mamufacex  21648  dmatelnd  21755  scmataddcl  21775  scmatsubcl  21776  scmatmulcl  21777  smatvscl  21783  mavmulsolcl  21810  mdetdiagid  21859  cramerlem3  21948  pmatcoe1fsupp  21960  cpmatacl  21975  cpmatmcllem  21977  mp2pm2mplem4  22068  chpscmat  22101  chfacfisf  22113  chfacfisfcpmat  22114  uniopn  22156  opnnei  22381  neindisj2  22384  restcls  22442  restntr  22443  tgcnp  22514  subbascn  22515  iscnp4  22524  lpcls  22625  cmpsublem  22660  cmpsub  22661  tgcmp  22662  cmpcld  22663  dfconn2  22680  1stcrest  22714  2ndcdisj  22717  1stccnp  22723  comppfsc  22793  kgencn2  22818  txlm  22909  kqreglem1  23002  filin  23115  isfil2  23117  ufilmax  23168  ufileu  23180  filufint  23181  cfinufil  23189  elfm2  23209  rnelfmlem  23213  rnelfm  23214  flimopn  23236  fbflim2  23238  flffbas  23256  fclsnei  23280  flimfnfcls  23289  fclscmp  23291  fcfnei  23296  cnpfcf  23302  alexsubALTlem2  23309  alexsubALTlem3  23310  alexsubALTlem4  23311  alexsubALT  23312  ptcmplem4  23316  qustgplem  23382  tsmsres  23405  tsmsxp  23416  metss  23774  metcnp3  23806  ovoliunnul  24781  ovolicc2lem3  24793  dyadmax  24872  itg2le  25014  bddiblnc  25116  itgcn  25119  ellimc3  25153  lhop1  25288  dvfsumrlim  25305  fta1g  25442  fta1  25578  aalioulem3  25604  aalioulem4  25605  ulmcaulem  25663  ulmcau  25664  logbgcd1irr  26054  xrlimcnp  26228  cxploglim  26237  jensen  26248  lgsqrmodndvds  26611  gausslemma2dlem1a  26623  gausslemma2dlem2  26625  gausslemma2dlem3  26626  lgsquad2lem2  26643  2lgslem1a1  26647  2sqlem6  26681  2sq2  26691  2sqnn  26697  2sqreultblem  26706  nosepdmlem  26941  nodenselem8  26949  madebdaylemlrcut  27134  brbtwn2  27628  ax5seglem5  27656  axcontlem4  27690  axcontlem10  27696  umgrnloopv  27831  umgrnloop  27833  upgredgpr  27867  numedglnl  27869  usgrausgrb  27894  usgrnloopvALT  27923  usgrnloopALT  27925  usgredg2vlem2  27948  ushgredgedg  27951  ushgredgedgloop  27953  upgrreslem  28026  umgrreslem  28027  nbgr0vtxlem  28077  nbusgrvtxm1  28101  uvtxnbgrvtx  28115  cusgredg  28146  cusgrres  28170  cusgrsize2inds  28175  cusgrfi  28180  fusgrregdegfi  28291  ewlkle  28327  uspgr2wlkeqi  28370  lfgrwlkprop  28409  lfgrwlknloop  28411  pthdivtx  28451  2pthnloop  28453  upgrwlkdvdelem  28458  upgrspthswlk  28460  usgr2wlkneq  28478  usgr2trlncl  28482  usgr2pthlem  28485  usgr2pth  28486  uspgrn2crct  28527  crctcshwlkn0lem4  28532  crctcshwlkn0lem5  28533  crctcshwlkn0  28540  wlkiswwlks1  28586  wlkiswwlks2  28594  wlkiswwlksupgr2  28596  wwlksnred  28611  wwlksnext  28612  wwlksnextbi  28613  wwlksnextwrd  28616  wwlksnextinj  28618  wwlksnextproplem2  28629  wwlksnextproplem3  28630  wspthsnonn0vne  28636  wspn0  28643  2pthon3v  28662  umgrwwlks2on  28676  elwspths2on  28679  wpthswwlks2on  28680  clwwlk1loop  28706  clwwlkccatlem  28707  umgrclwwlkge2  28709  clwlkclwwlklem2a4  28715  clwlkclwwlklem2a  28716  clwlkclwwlklem3  28719  clwlkclwwlkf1lem3  28724  clwlkclwwlkfo  28727  clwwisshclwwslemlem  28731  erclwwlkeqlen  28737  erclwwlksym  28739  clwwlkf  28765  clwwlknscsh  28780  erclwwlknsym  28788  clwwlknonex2lem2  28826  clwwlknonex2  28827  upgr3v3e3cycl  28898  upgr4cycl4dv4e  28903  eucrctshift  28961  3vfriswmgr  28996  1to2vfriswmgr  28997  1to3vfriswmgr  28998  n4cyclfrgr  29009  4cyclusnfrgr  29010  frgrnbnb  29011  frgrncvvdeqlem8  29024  frgrwopreg  29041  frgr2wwlk1  29047  frgr2wwlkeqm  29049  2clwwlk2clwwlklem  29064  numclwwlk1lem2fo  29076  wlkl0  29085  numclwlk2lem2f  29095  frgrreggt1  29111  frgrreg  29112  frgrregord013  29113  frgrregord13  29114  frgrogt3nreg  29115  eulplig  29201  nmoub3i  29489  ipasslem5  29551  htthlem  29633  ocin  30012  spansneleq  30286  spansnss  30287  elspansn4  30289  h1datomi  30297  nmopub2tALT  30625  nmfnleub2  30642  hstel2  30935  cvnbtwn  31002  spansncv2  31009  dmdmd  31016  dmdbr3  31021  dmdbr4  31022  dmdbr5  31024  mdsl0  31026  mdexchi  31051  cvexchlem  31084  atcv1  31096  atomli  31098  atcvatlem  31101  atcvat2i  31103  chirredi  31110  mdsymlem3  31121  mdsymlem4  31122  sumdmdii  31131  sumdmdlem  31134  cdj1i  31149  ssrelf  31306  f1o3d  31313  fisshasheq  33436  umgr2cycllem  33465  cvxpconn  33567  satfv0  33683  satfsschain  33689  satfrel  33692  satfdm  33694  satfv0fun  33696  sat1el2xp  33704  gonarlem  33719  goalrlem  33721  satffunlem1lem1  33727  satffunlem2lem1  33729  satffunlem2lem2  33731  satffun  33734  mrsubccat  33843  msubvrs  33885  fundmpss  34089  dfon2lem6  34111  dfon2lem8  34113  dfon2lem9  34114  dfon2  34115  wzel  34161  addsprop  34242  addsunif  34258  colinearxfr  34516  btwnconn1lem11  34538  lineintmo  34598  trer  34644  elicc3  34645  finminlem  34646  nn0prpwlem  34650  fnessref  34685  neibastop2  34689  fgmin  34698  tailfb  34705  ordcmp  34775  ee7.2aOLD  34789  bj-cbvalimt  34959  bj-ceqsalt0  35207  bj-ceqsalt1  35208  isbasisrelowllem1  35682  isbasisrelowllem2  35683  relowlpssretop  35691  fvineqsneu  35738  fvineqsneq  35739  wl-mo3t  35887  finixpnum  35918  matunitlindflem1  35929  matunitlindflem2  35930  poimirlem26  35959  poimirlem27  35960  poimirlem29  35962  ftc1anc  36014  fdc  36059  heibor1lem  36123  ghomco  36205  rngoueqz  36254  unichnidl  36345  dmncan1  36390  ax12indn  37261  lshpdisj  37305  lub0N  37507  glb0N  37511  leat2  37612  hlrelat2  37722  cvrexchlem  37738  cvratlem  37740  atcvrj0  37747  cvrat2  37748  snatpsubN  38069  linepsubN  38071  pmaple  38080  pmapsub  38087  elpaddn0  38119  paddasslem5  38143  trlval2  38482  cdlemn11pre  39529  dihord2pre  39544  mapdordlem2  39956  fsuppind  40590  sn-sup2  40750  pell1qrgap  41009  dford3lem1  41162  hbtlem5  41267  omcl2  41370  ntrneiiso  42074  sbiota1  42425  19.41rg  42543  ee223  42627  or2expropbilem1  44944  funressnfv  44955  fcoresf1  44981  2reuimp  45025  f1oresf1o2  45201  zm1nn  45212  nltle2tri  45223  el1fzopredsuc  45235  fzoopth  45237  elsetpreimafvssdm  45256  imasetpreimafvbijlemf1  45274  iccpartlt  45294  iccpartgt  45297  iccelpart  45303  icceuelpart  45306  iccpartnel  45308  fargshiftfo  45312  fargshiftfva  45313  lswn0  45314  ich2exprop  45341  prsprel  45357  sprsymrelfolem2  45363  sprsymrelfo  45367  poprelb  45394  reuopreuprim  45396  goldbachthlem2  45416  odz2prm2pw  45433  fmtnoprmfac1  45435  fmtnofac2lem  45438  prmdvdsfmtnof1lem2  45455  2pwp1prm  45459  sfprmdvdsmersenne  45473  lighneallem3  45477  requad01  45491  requad2  45493  even3prm2  45589  fppr2odd  45601  fpprwpprb  45610  gbegt5  45631  sbgoldbwt  45647  sbgoldbalt  45651  sbgoldbm  45654  bgoldbtbndlem2  45676  bgoldbtbndlem3  45677  bgoldbtbndlem4  45678  bgoldbtbnd  45679  tgblthelfgott  45685  tgoldbach  45687  isomuspgrlem2b  45699  isomuspgrlem2d  45701  isomuspgr  45704  isomgrsym  45706  upgrwlkupwlk  45720  lmod0rng  45844  nzerooringczr  46048  ztprmneprm  46101  ply1mulgsumlem1  46145  ply1mulgsumlem2  46146  lcoel0  46187  linindslinci  46207  lindslinindimp2lem4  46220  lindslinindsimp2lem5  46221  snlindsntor  46230  ldepspr  46232  lincresunit2  46237  fllog2  46332  dignn0ldlem  46366  dignn0flhalflem1  46379  nn0sumshdiglemA  46383  nn0sumshdiglemB  46384  itcovalt2  46441  resum2sqorgt0  46473  eenglngeehlnmlem2  46502  rrx2linest  46506  itscnhlc0xyqsol  46529  itsclc0  46535  setrec1lem2  46811  aacllem  46922