MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  com23 Structured version   Visualization version   GIF version

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
StepHypRef Expression
1 com3.1 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
2 pm2.27 42 . 2 (𝜒 → ((𝜒𝜃) → 𝜃))
31, 2syl9 77 1 (𝜑 → (𝜒 → (𝜓𝜃)))
Colors of variables: wff setvar class
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  412  expcomd  417  impancom  452  a2and  839  dedlem0b  1036  sbequ1  2240  moexexlem  2707  ralrimdvva  3194  ceqsalt  3528  vtoclgft  3554  vtoclgftOLD  3555  sbciegft  3807  reupick  4286  reusv3  5297  sbcop1  5371  propeqop  5389  pwssun  5449  wefrc  5543  ssrel  5651  ssrel2  5653  ssrelrel  5663  ssrelrn  5757  predpo  6160  tz7.7  6211  ordtr2  6229  onmindif  6274  unizlim  6301  funssres  6392  f1ssf1  6640  fvmptt  6781  fveqdmss  6839  fvcofneq  6852  funsndifnop  6906  funfvima2  6985  isoini  7080  isopolem  7087  weniso  7096  f1ocnv2d  7387  limsssuc  7553  tfindsg  7563  limomss  7573  findsg  7597  funcnvuni  7624  f1oweALT  7664  funelss  7737  bropopvvv  7776  bropfvvvvlem  7777  bropfvvvv  7778  f1o2ndf1  7809  frxp  7811  suppfnss  7846  wfrlem12  7957  onfununi  7969  tz7.49  8072  omordi  8182  omlimcl  8194  omass  8196  oeordsuc  8210  nnmordi  8247  nnmord  8248  omabs  8264  xpdom2  8601  infensuc  8684  findcard2  8747  findcard2d  8749  findcard3  8750  frfi  8752  xpfi  8778  fsuppres  8847  dffi2  8876  elfiun  8883  ordiso2  8968  ordtypelem7  8977  suc11reg  9071  inf3lem2  9081  noinfep  9112  cantnfle  9123  cantnflem1  9141  cantnf  9145  trcl  9159  epfrs  9162  r1sdom  9192  updjud  9352  pr2ne  9420  dfac8alem  9444  indcardi  9456  alephordi  9489  dfac12lem3  9560  pwsdompw  9615  cofsmo  9680  cfcoflem  9683  coftr  9684  isf32lem2  9765  isf32lem9  9772  axcc3  9849  domtriomlem  9853  axdc3lem2  9862  axdc3lem4  9864  zorn2lem4  9910  zorn2lem6  9912  zorn2lem7  9913  ttukeylem6  9925  uniimadom  9955  konigthlem  9979  fpwwe2lem8  10048  tskord  10191  tskcard  10192  grupr  10208  gruiin  10221  grudomon  10228  grur1a  10230  genpn0  10414  genpcd  10417  distrlem5pr  10438  psslinpr  10442  ltaddpr  10445  ltexprlem3  10449  ltexprlem6  10452  ltapr  10456  prlem936  10458  suplem1pr  10463  axpre-sup  10580  1re  10630  dedekindle  10793  lemul12a  11487  divgt0  11497  divge0  11498  lbreu  11580  sup2  11586  bndndx  11885  elnnz  11980  nzadd  12019  fzind  12069  fnn0ind  12070  uzwo  12300  lbzbi  12325  zmax  12334  zbtwnre  12335  irradd  12362  irrmul  12363  ledivge1le  12450  xrub  12695  supxrunb2  12703  infmremnf  12726  iccid  12773  uzsubsubfz  12919  fzrevral  12982  elfz0fzfz0  13002  fz0fzelfz0  13003  elfzmlbp  13008  elincfzoext  13085  ssfzoulel  13121  ssfzo12bi  13122  elfzonelfzo  13129  elfznelfzo  13132  elfznelfzob  13133  injresinjlem  13147  fleqceilz  13212  modaddmodup  13292  uzindi  13340  suppssfz  13352  mptnn0fsuppr  13357  le2sq2  13490  sqlecan  13561  facdiv  13637  facwordi  13639  faclbnd  13640  hashimarni  13792  hash2prd  13823  hashle2pr  13825  pr2pwpr  13827  fundmge2nop0  13840  fi1uzind  13845  brfi1indALT  13848  swrdnd2  14007  swrdnnn0nd  14008  swrdnd0  14009  pfxnd0  14040  swrdswrdlem  14056  swrdswrd  14057  ccatopth2  14069  wrd2ind  14075  pfxccatin12lem2a  14079  swrdccatin2  14081  pfxccatin12lem2  14083  pfxccatin12lem3  14084  swrdccat  14087  swrdccat3blem  14091  reuccatpfxs1lem  14098  repswswrd  14136  cshwidxmod  14155  cshwidx0  14158  2cshwcshw  14177  cshwcsh2id  14180  cau3lem  14704  caubnd  14708  climrlim2  14894  rlimcn2  14937  mulcn2  14942  climcau  15017  climbdd  15018  caucvg  15025  modfsummod  15139  p1modz1  15604  dvdsle  15650  dvdsdivcl  15656  ltoddhalfle  15700  halfleoddlt  15701  ndvdssub  15750  gcdcllem1  15838  dvdslegcd  15843  bezoutlem4  15880  dfgcd2  15884  lcmf  15967  lcmfunsnlem1  15971  lcmfunsnlem2lem1  15972  lcmfunsnlem  15975  lcmfdvdsb  15977  lcmfun  15979  coprmdvds1  15986  divgcdcoprm0  15999  cncongr1  16001  cncongr2  16002  prmfac1  16053  pcqcl  16183  dvdsprmpweqle  16212  oddprmdvds  16229  prmpwdvds  16230  infpnlem1  16236  prmgaplem5  16381  prmgaplem6  16382  prmgaplem7  16383  cshwshashlem1  16419  cictr  17065  initoeu2lem1  17264  initoeu2  17266  clatleglb  17726  lidrididd  17870  mulgaddcom  18191  mulginvcom  18192  cycsubm  18285  cyccom  18286  gsmsymgreqlem2  18490  symggen  18529  psgnunilem4  18556  sylow2blem3  18678  frgpnabllem1  18924  dprddisj2  19092  f1rhm0to0ALT  19425  lmodfopnelem1  19601  lssssr  19656  lss1d  19666  lspsncv0  19849  mplcoe5lem  20178  cply1mul  20392  coe1fzgsumdlem  20399  gsummoncoe1  20402  evl1gsumdlem  20449  znrrg  20642  mamufacex  20930  dmatelnd  21035  scmataddcl  21055  scmatsubcl  21056  scmatmulcl  21057  smatvscl  21063  mavmulsolcl  21090  mdetdiagid  21139  cramerlem3  21228  pmatcoe1fsupp  21239  cpmatacl  21254  cpmatmcllem  21256  mp2pm2mplem4  21347  chpscmat  21380  chfacfisf  21392  chfacfisfcpmat  21393  uniopn  21435  opnnei  21658  neindisj2  21661  restcls  21719  restntr  21720  tgcnp  21791  subbascn  21792  iscnp4  21801  lpcls  21902  cmpsublem  21937  cmpsub  21938  tgcmp  21939  cmpcld  21940  dfconn2  21957  1stcrest  21991  2ndcdisj  21994  1stccnp  22000  comppfsc  22070  kgencn2  22095  txlm  22186  kqreglem1  22279  filin  22392  isfil2  22394  ufilmax  22445  ufileu  22457  filufint  22458  cfinufil  22466  elfm2  22486  rnelfmlem  22490  rnelfm  22491  flimopn  22513  fbflim2  22515  flffbas  22533  fclsnei  22557  flimfnfcls  22566  fclscmp  22568  fcfnei  22573  cnpfcf  22579  alexsubALTlem2  22586  alexsubALTlem3  22587  alexsubALTlem4  22588  alexsubALT  22589  ptcmplem4  22593  qustgplem  22658  tsmsres  22681  tsmsxp  22692  metss  23047  metcnp3  23079  ovoliunnul  24037  ovolicc2lem3  24049  dyadmax  24128  itg2le  24269  itgcn  24372  ellimc3  24406  lhop1  24540  dvfsumrlim  24557  fta1g  24690  fta1  24826  aalioulem3  24852  aalioulem4  24853  ulmcaulem  24911  ulmcau  24912  logbgcd1irr  25299  xrlimcnp  25474  cxploglim  25483  jensen  25494  lgsqrmodndvds  25857  gausslemma2dlem1a  25869  gausslemma2dlem2  25871  gausslemma2dlem3  25872  lgsquad2lem2  25889  2lgslem1a1  25893  2sqlem6  25927  2sq2  25937  2sqnn  25943  2sqreultblem  25952  brbtwn2  26619  ax5seglem5  26647  axcontlem4  26681  axcontlem10  26687  umgrnloopv  26819  umgrnloop  26821  upgredgpr  26855  numedglnl  26857  usgrausgrb  26882  usgrnloopvALT  26911  usgrnloopALT  26913  usgredg2vlem2  26936  ushgredgedg  26939  ushgredgedgloop  26941  upgrreslem  27014  umgrreslem  27015  nbgr0vtxlem  27065  nbusgrvtxm1  27089  uvtxnbgrvtx  27103  cusgredg  27134  cusgrres  27158  cusgrsize2inds  27163  cusgrfi  27168  fusgrregdegfi  27279  ewlkle  27315  uspgr2wlkeqi  27357  wlklenvclwlkOLD  27365  lfgrwlkprop  27397  lfgrwlknloop  27399  pthdivtx  27438  2pthnloop  27440  upgrwlkdvdelem  27445  upgrspthswlk  27447  usgr2wlkneq  27465  usgr2trlncl  27469  usgr2pthlem  27472  usgr2pth  27473  uspgrn2crct  27514  crctcshwlkn0lem4  27519  crctcshwlkn0lem5  27520  crctcshwlkn0  27527  wlkiswwlks1  27573  wlkiswwlks2  27581  wlkiswwlksupgr2  27583  wwlksnred  27598  wwlksnext  27599  wwlksnextbi  27600  wwlksnextwrd  27603  wwlksnextinj  27605  wwlksnextproplem2  27617  wwlksnextproplem3  27618  wspthsnonn0vne  27624  wspn0  27631  2pthon3v  27650  umgrwwlks2on  27664  elwspths2on  27667  wpthswwlks2on  27668  clwwlk1loop  27694  clwwlkccatlem  27695  umgrclwwlkge2  27697  clwlkclwwlklem2a4  27703  clwlkclwwlklem2a  27704  clwlkclwwlklem3  27707  clwlkclwwlkf1lem3  27712  clwlkclwwlkfo  27715  clwwisshclwwslemlem  27719  erclwwlkeqlen  27725  erclwwlksym  27727  clwwlkf  27754  clwwlknscsh  27769  erclwwlknsym  27777  clwwlknonex2lem2  27815  clwwlknonex2  27816  upgr3v3e3cycl  27887  upgr4cycl4dv4e  27892  eucrctshift  27950  3vfriswmgr  27985  1to2vfriswmgr  27986  1to3vfriswmgr  27987  n4cyclfrgr  27998  4cyclusnfrgr  27999  frgrnbnb  28000  frgrncvvdeqlem8  28013  frgrwopreg  28030  frgr2wwlk1  28036  frgr2wwlkeqm  28038  2clwwlk2clwwlklem  28053  numclwwlk1lem2fo  28065  wlkl0  28074  numclwlk2lem2f  28084  frgrreggt1  28100  frgrreg  28101  frgrregord013  28102  frgrregord13  28103  frgrogt3nreg  28104  eulplig  28190  nmoub3i  28478  ipasslem5  28540  htthlem  28622  ocin  29001  spansneleq  29275  spansnss  29276  elspansn4  29278  h1datomi  29286  nmopub2tALT  29614  nmfnleub2  29631  hstel2  29924  cvnbtwn  29991  spansncv2  29998  dmdmd  30005  dmdbr3  30010  dmdbr4  30011  dmdbr5  30013  mdsl0  30015  mdexchi  30040  cvexchlem  30073  atcv1  30085  atomli  30087  atcvatlem  30090  atcvat2i  30092  chirredi  30099  mdsymlem3  30110  mdsymlem4  30111  sumdmdii  30120  sumdmdlem  30123  cdj1i  30138  ssrelf  30295  f1o3d  30301  fisshasheq  32250  umgr2cycllem  32285  cvxpconn  32387  satfv0  32503  satfsschain  32509  satfrel  32512  satfdm  32514  satfv0fun  32516  sat1el2xp  32524  gonarlem  32539  goalrlem  32541  satffunlem1lem1  32547  satffunlem2lem1  32549  satffunlem2lem2  32551  satffun  32554  mrsubccat  32663  msubvrs  32705  fundmpss  32907  dfon2lem6  32931  dfon2lem8  32933  dfon2lem9  32934  dfon2  32935  trpredrec  32975  soseq  32994  wzel  33009  frr3g  33019  nosepdmlem  33085  nodenselem8  33093  colinearxfr  33434  btwnconn1lem11  33456  lineintmo  33516  trer  33562  elicc3  33563  finminlem  33564  nn0prpwlem  33568  fnessref  33603  neibastop2  33607  fgmin  33616  tailfb  33623  ordcmp  33693  ee7.2aOLD  33707  bj-cbvalimt  33870  bj-ceqsalt0  34098  bj-ceqsalt1  34099  isbasisrelowllem1  34519  isbasisrelowllem2  34520  relowlpssretop  34528  fvineqsneu  34575  fvineqsneq  34576  wl-mo3t  34694  finixpnum  34759  matunitlindflem1  34770  matunitlindflem2  34771  poimirlem26  34800  poimirlem27  34801  poimirlem29  34803  bddiblnc  34844  ftc1anc  34857  fdc  34903  heibor1lem  34970  ghomco  35052  rngoueqz  35101  unichnidl  35192  dmncan1  35237  ax12indn  35961  lshpdisj  36005  lub0N  36207  glb0N  36211  leat2  36312  hlrelat2  36421  cvrexchlem  36437  cvratlem  36439  atcvrj0  36446  cvrat2  36447  snatpsubN  36768  linepsubN  36770  pmaple  36779  pmapsub  36786  elpaddn0  36818  paddasslem5  36842  trlval2  37181  cdlemn11pre  38228  dihord2pre  38243  mapdordlem2  38655  pell1qrgap  39351  dford3lem1  39503  hbtlem5  39608  ntrneiiso  40321  sbiota1  40646  19.41rg  40764  ee223  40848  or2expropbilem1  43148  funressnfv  43159  2reuimp  43195  f1oresf1o2  43371  zm1nn  43383  nltle2tri  43394  el1fzopredsuc  43406  fzoopth  43408  iccpartlt  43431  iccpartgt  43434  iccelpart  43440  icceuelpart  43443  iccpartnel  43445  fargshiftfo  43449  fargshiftfva  43450  lswn0  43451  ich2exprop  43480  prsprel  43496  sprsymrelfolem2  43502  sprsymrelfo  43506  poprelb  43533  reuopreuprim  43535  goldbachthlem2  43555  odz2prm2pw  43572  fmtnoprmfac1  43574  fmtnofac2lem  43577  prmdvdsfmtnof1lem2  43594  2pwp1prm  43598  sfprmdvdsmersenne  43615  lighneallem3  43619  requad01  43633  requad2  43635  even3prm2  43731  fppr2odd  43743  fpprwpprb  43752  gbegt5  43773  sbgoldbwt  43789  sbgoldbalt  43793  sbgoldbm  43796  bgoldbtbndlem2  43818  bgoldbtbndlem3  43819  bgoldbtbndlem4  43820  bgoldbtbnd  43821  tgblthelfgott  43827  tgoldbach  43829  isomuspgrlem2b  43841  isomuspgrlem2d  43843  isomuspgr  43846  isomgrsym  43848  upgrwlkupwlk  43862  lmod0rng  44037  nzerooringczr  44241  ztprmneprm  44293  ply1mulgsumlem1  44338  ply1mulgsumlem2  44339  lcoel0  44381  linindslinci  44401  lindslinindimp2lem4  44414  lindslinindsimp2lem5  44415  snlindsntor  44424  ldepspr  44426  lincresunit2  44431  fllog2  44526  dignn0ldlem  44560  dignn0flhalflem1  44573  nn0sumshdiglemA  44577  nn0sumshdiglemB  44578  resum2sqorgt0  44594  eenglngeehlnmlem2  44623  rrx2linest  44627  itscnhlc0xyqsol  44650  itsclc0  44656  setrec1lem2  44689  aacllem  44800
  Copyright terms: Public domain W3C validator