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  107  expcomd  453  impancom  455  a2and  888  dedlem0b  1031  ad5ant13OLD  1193  ad5ant14OLD  1195  ad5ant15OLD  1197  3com23OLD  1422  ad5ant134OLD  1454  ad5ant135OLD  1456  moexex  2667  ralrimdvva  3100  ceqsalt  3356  vtoclgft  3382  vtoclgftOLD  3383  reu6  3524  sbciegft  3595  reupick  4042  reusv3  5013  ralxfrd  5016  ralxfrd2  5021  propeqop  5106  pwssun  5158  wefrc  5248  ssrel  5352  ssrelOLD  5353  ssrel2  5355  ssrelrel  5365  ssrelrn  5458  predpo  5847  tz7.7  5898  ordtr2  5917  onmindif  5964  unizlim  5993  funssres  6079  f1ssf1  6317  fv3  6355  fvmptt  6450  fveqdmss  6505  fvcofneq  6518  funsndifnop  6567  fmptsnd  6587  funfvima2  6644  isoini  6739  isopolem  6746  weniso  6755  f1ocnv2d  7039  limsssuc  7203  tfindsg  7213  limomss  7223  findsg  7246  funcnvuni  7272  f1oweALT  7305  bropopvvv  7411  bropfvvvvlem  7412  bropfvvvv  7413  f1o2ndf1  7441  frxp  7443  suppfnss  7476  suppfnssOLD  7477  wfr3g  7570  wfrlem12  7583  onfununi  7595  tz7.49  7697  omordi  7803  omlimcl  7815  omass  7817  oeordsuc  7831  nnmordi  7868  nnmord  7869  omabs  7884  xpdom2  8208  infensuc  8291  findcard2  8353  findcard2d  8355  findcard3  8356  frfi  8358  xpfi  8384  fsuppres  8453  dffi2  8482  elfiun  8489  ordiso2  8573  ordtypelem7  8582  suc11reg  8677  inf3lem2  8687  noinfep  8718  cantnfle  8729  cantnflem1  8747  cantnf  8751  trcl  8765  epfrs  8768  r1sdom  8798  pr2ne  8989  dfac8alem  9013  indcardi  9025  alephordi  9058  dfac12lem3  9130  pwsdompw  9189  cofsmo  9254  cfcoflem  9257  coftr  9258  isf32lem2  9339  isf32lem9  9346  axcc3  9423  domtriomlem  9427  axdc3lem2  9436  axdc3lem4  9438  zorn2lem4  9484  zorn2lem6  9486  zorn2lem7  9487  ttukeylem6  9499  uniimadom  9529  konigthlem  9553  fpwwe2lem8  9622  tskord  9765  tskcard  9766  grupr  9782  gruiin  9795  grudomon  9802  grur1a  9804  nqereu  9914  genpn0  9988  genpcd  9991  distrlem5pr  10012  psslinpr  10016  ltaddpr  10019  ltexprlem3  10023  ltexprlem6  10026  ltapr  10030  prlem936  10032  suplem1pr  10037  axpre-sup  10153  1re  10202  ltletr  10292  dedekindle  10364  lemul12a  11044  divgt0  11054  divge0  11055  lbreu  11136  sup2  11142  bndndx  11454  elnnz  11550  nzadd  11588  fzind  11638  fnn0ind  11639  uzwo  11915  eqreznegel  11938  lbzbi  11940  zmax  11949  zbtwnre  11950  irradd  11976  irrmul  11977  ledivge1le  12065  xrltletr  12152  xnn0xaddcl  12230  xrub  12306  supxrunb2  12314  infmremnf  12337  iccid  12384  uzsubsubfz  12527  fzrevral  12589  elfz0fzfz0  12609  fz0fzelfz0  12610  elfzmlbp  12615  elincfzoext  12691  elfzodifsumelfzo  12699  ssfzoulel  12727  ssfzo12bi  12728  elfzonelfzo  12735  elfznelfzo  12738  elfznelfzob  12739  injresinjlem  12753  fleqceilz  12818  modaddmodup  12898  uzindi  12946  suppssfz  12959  mptnn0fsuppr  12964  le2sq2  13104  sqlecan  13136  facdiv  13239  facwordi  13241  faclbnd  13242  hashimarni  13391  hash2prd  13420  hashle2pr  13422  pr2pwpr  13424  fundmge2nop0  13437  fi1uzind  13442  brfi1indALT  13445  swrdnd2  13604  swrdswrdlem  13630  swrdswrd  13631  ccatopth2  13642  wrd2ind  13648  reuccats1lem  13650  swrdccatin1  13654  swrdccatin12lem2a  13656  swrdccatin2  13658  swrdccatin12lem2  13660  swrdccatin12lem3  13661  swrdccat  13664  swrdccat3blem  13666  repswswrd  13702  cshwidxmod  13720  cshwidx0  13723  2cshwcshw  13742  cshwcsh2id  13745  cau3lem  14264  caubnd  14268  climrlim2  14448  rlimuni  14451  rlimcn2  14491  mulcn2  14496  rlimno1  14554  climcau  14571  climbdd  14572  caucvg  14579  modfsummod  14696  p1modz1  15160  dvdsle  15205  dvdsdivcl  15211  ltoddhalfle  15258  halfleoddlt  15259  ndvdssub  15306  gcdcllem1  15394  dvdslegcd  15399  bezoutlem4  15432  dfgcd2  15436  lcmf  15519  lcmfunsnlem1  15523  lcmfunsnlem2lem1  15524  lcmfunsnlem2  15526  lcmfunsnlem  15527  lcmfdvdsb  15529  lcmfun  15531  coprmdvds1  15538  coprmdvds  15539  coprmdvdsOLD  15540  coprmdvds2  15541  divgcdcoprm0  15552  cncongr1  15554  cncongr2  15555  prmfac1  15604  pcqcl  15734  dvdsprmpweqle  15763  oddprmdvds  15780  prmpwdvds  15781  infpnlem1  15787  prmgaplem5  15932  prmgaplem6  15933  prmgaplem7  15934  cshwshashlem1  15975  cictr  16637  initoeu2lem1  16836  initoeu2  16838  clatleglb  17298  mulgaddcom  17736  mulginvcom  17737  gsmsymgrfixlem1  18018  gsmsymgreqlem2  18022  symggen  18061  psgnunilem4  18088  sylow2blem3  18208  lsmdisj2  18266  frgpnabllem1  18447  dprddisj2  18609  f1rhm0to0ALT  18914  lmodfopnelem1  19072  lssssr  19126  lss1d  19136  lspsncv0  19319  mplcoe5lem  19640  cply1mul  19837  coe1fzgsumdlem  19844  gsummoncoe1  19847  evl1gsumdlem  19893  znrrg  20087  mamufacex  20368  dmatelnd  20475  scmataddcl  20495  scmatsubcl  20496  scmatmulcl  20497  smatvscl  20503  mavmulsolcl  20530  mdetdiagid  20579  cramerlem3  20668  pmatcoe1fsupp  20679  cpmatacl  20694  cpmatmcllem  20696  mp2pm2mplem4  20787  chpscmat  20820  chfacfisf  20832  chfacfisfcpmat  20833  uniopn  20875  opnnei  21097  neindisj2  21100  restcls  21158  restntr  21159  tgcnp  21230  subbascn  21231  iscnp4  21240  lmcnp  21281  lpcls  21341  cmpsublem  21375  cmpsub  21376  tgcmp  21377  cmpcld  21378  dfconn2  21395  1stcrest  21429  2ndcdisj  21432  1stccnp  21438  comppfsc  21508  kgencn2  21533  txlm  21624  kqreglem1  21717  filin  21830  isfil2  21832  fgss2  21850  fgfil  21851  ufilmax  21883  ufileu  21895  filufint  21896  cfinufil  21904  elfm2  21924  rnelfmlem  21928  rnelfm  21929  fmfnfmlem2  21931  fmfnfmlem4  21933  flimopn  21951  fbflim2  21953  flffbas  21971  fclsnei  21995  flimfnfcls  22004  fclscmp  22006  ufilcmp  22008  fcfnei  22011  cnpfcf  22017  alexsubALTlem2  22024  alexsubALTlem3  22025  alexsubALTlem4  22026  alexsubALT  22027  ptcmplem4  22031  qustgplem  22096  tsmsres  22119  tsmsxp  22130  metss  22485  metcnp3  22517  ivthlem2  23392  ivthlem3  23393  ovoliunnul  23446  ovolicc2lem3  23458  dyadmax  23537  itg2le  23676  itgcn  23779  ellimc3  23813  lhop1  23947  dvfsumrlim  23964  fta1g  24097  fta1  24233  aalioulem3  24259  aalioulem4  24260  ulmcaulem  24318  ulmcau  24319  xrlimcnp  24865  cxploglim  24874  jensen  24885  lgsqrmodndvds  25248  gausslemma2dlem1a  25260  gausslemma2dlem2  25262  gausslemma2dlem3  25263  lgsquad2lem2  25280  2lgslem1a1  25284  2sqlem6  25318  brbtwn2  25955  ax5seglem5  25983  axcontlem4  26017  axcontlem10  26023  umgrnloopv  26171  umgrnloop  26173  umgrislfupgrlem  26187  upgredgpr  26207  numedglnl  26209  usgrausgrb  26234  usgrnloopvALT  26263  usgrnloopALT  26265  uhgr2edg  26270  usgredg2vlem2  26288  ushgredgedg  26291  ushgredgedgloop  26293  upgrreslem  26366  umgrreslem  26367  nbgr0vtxlem  26421  nbusgrvtxm1  26450  uvtxnbgrvtx  26466  cusgredg  26501  cusgrres  26525  cusgrsize2inds  26530  cusgrfi  26535  fusgrregdegfi  26646  ewlkle  26682  upgrewlkle2  26683  uspgr2wlkeqi  26725  wlkv0  26728  wlklenvclwlk  26732  lfgrwlkprop  26765  lfgrwlknloop  26767  pthdivtx  26806  2pthnloop  26808  upgrwlkdvdelem  26813  upgrspthswlk  26815  usgr2wlkneq  26833  usgr2trlncl  26837  usgr2pthlem  26840  usgr2pth  26841  uspgrn2crct  26882  crctcshwlkn0lem4  26887  crctcshwlkn0lem5  26888  crctcshwlkn0  26895  wlkiswwlks1  26947  wlkiswwlks2  26955  wlkiswwlksupgr2  26957  wwlksnred  26981  wwlksnext  26982  wwlksnextbi  26983  wwlksnextwrd  26986  wwlksnextinj  26988  wwlksnextproplem2  26999  wwlksnextproplem3  27000  wspthsnonn0vne  27008  wspn0  27015  2pthon3v  27034  umgrwwlks2on  27049  elwspths2on  27052  wpthswwlks2on  27053  wpthswwlks2onOLD  27054  clwwlk1loop  27082  clwwlkccatlem  27083  umgrclwwlkge2  27085  clwlkclwwlklem2a4  27091  clwlkclwwlklem2a  27092  clwlkclwwlklem3  27095  clwlkclwwlkf1lem3  27100  clwlkclwwlkfo  27103  clwwisshclwwslemlem  27107  erclwwlkeqlen  27113  erclwwlksym  27115  clwwlkf  27147  wwlksext2clwwlkOLD  27159  clwwlknscsh  27164  erclwwlknsym  27172  clwlksfclwwlkOLD  27187  clwwlknonwwlknonbOLD  27226  clwwlknonex2lem2  27228  clwwlknonex2  27229  upgr3v3e3cycl  27303  upgr4cycl4dv4e  27308  eucrctshift  27366  3vfriswmgr  27403  1to2vfriswmgr  27404  1to3vfriswmgr  27405  n4cyclfrgr  27416  4cyclusnfrgr  27417  frgrnbnb  27418  frgrncvvdeqlem8  27431  frgrwopreg  27448  frgr2wwlk1  27454  frgr2wwlkeqm  27456  numclwwlk2lem1lemOLD  27470  2clwwlk2clwwlklem  27474  numclwlk1lem2fo  27488  wlkl0  27499  numclwlk2lem2f  27509  numclwlk2lem2fOLD  27516  frgrreggt1  27532  frgrreg  27533  frgrregord013  27534  frgrregord13  27535  frgrogt3nreg  27536  eulplig  27619  nmoub3i  27908  ipasslem5  27970  htthlem  28054  ocin  28435  spansneleq  28709  spansnss  28710  elspansn4  28712  h1datomi  28720  nmopub2tALT  29048  nmfnleub2  29065  hstel2  29358  cvnbtwn  29425  spansncv2  29432  dmdmd  29439  dmdbr3  29444  dmdbr4  29445  dmdbr5  29447  mdsl0  29449  mdexchi  29474  cvexchlem  29507  atcv1  29519  atomli  29521  atcvatlem  29524  atcvat2i  29526  chirredi  29533  mdsymlem3  29544  mdsymlem4  29545  sumdmdii  29554  sumdmdlem  29557  cdj1i  29572  ssrelf  29705  f1o3d  29711  cvxpconn  31502  mrsubccat  31693  msubvrs  31735  fundmpss  31942  dfon2lem6  31969  dfon2lem8  31971  dfon2lem9  31972  dfon2  31973  trpredrec  32014  soseq  32031  wzel  32046  frr3g  32056  nosepdmlem  32110  nodenselem8  32118  colinearxfr  32459  btwnconn1lem11  32481  lineintmo  32541  trer  32587  elicc3  32588  finminlem  32589  nn0prpwlem  32594  fnessref  32629  neibastop2  32633  fgmin  32642  tailfb  32649  ordcmp  32723  ee7.2aOLD  32737  bj-ceqsalt0  33150  bj-ceqsalt1  33151  isbasisrelowllem1  33485  isbasisrelowllem2  33486  relowlpssretop  33494  wl-mo3t  33640  finixpnum  33676  matunitlindflem1  33687  matunitlindflem2  33688  poimirlem26  33717  poimirlem27  33718  poimirlem29  33720  bddiblnc  33762  ftc1anc  33775  fdc  33823  heibor1lem  33890  ghomco  33972  rngoueqz  34021  unichnidl  34112  dmncan1  34157  ax12indn  34701  lshpdisj  34746  lub0N  34948  glb0N  34952  leat2  35053  hlrelat2  35161  cvrexchlem  35177  cvratlem  35179  atcvrj0  35186  cvrat2  35187  snatpsubN  35508  linepsubN  35510  pmaple  35519  pmapsub  35526  elpaddn0  35558  paddasslem5  35582  trlval2  35922  cdlemn11pre  36970  dihord2pre  36985  mapdordlem2  37397  pell1qrgap  37909  dford3lem1  38064  hbtlem5  38169  ntrneiiso  38860  sbiota1  39106  19.41rg  39237  ee223  39330  funressnfv  41683  zm1nn  41795  nltle2tri  41802  el1fzopredsuc  41814  fzoopth  41816  iccpartlt  41839  iccpartgt  41842  iccelpart  41848  icceuelpart  41851  iccpartnel  41853  fargshiftfo  41857  fargshiftfva  41858  lswn0  41859  pfxccatin12lem2  41903  reuccatpfxs1lem  41912  goldbachthlem2  41937  odz2prm2pw  41954  fmtnoprmfac1  41956  fmtnofac2lem  41959  prmdvdsfmtnof1lem2  41976  2pwp1prm  41982  sfprmdvdsmersenne  41999  lighneallem3  42003  even3prm2  42107  gbegt5  42128  sbgoldbwt  42144  sbgoldbalt  42148  sbgoldbm  42151  bgoldbtbndlem2  42173  bgoldbtbndlem3  42174  bgoldbtbndlem4  42175  bgoldbtbnd  42176  tgblthelfgott  42182  tgoldbach  42184  tgblthelfgottOLD  42188  tgoldbachOLD  42191  upgrwlkupwlk  42200  prsprel  42216  sprsymrelfolem2  42222  sprsymrelfo  42226  lmod0rng  42347  nzerooringczr  42551  ztprmneprm  42604  ply1mulgsumlem1  42653  ply1mulgsumlem2  42654  lcoel0  42696  linindslinci  42716  lindslinindimp2lem4  42729  lindslinindsimp2lem5  42730  snlindsntor  42739  ldepspr  42741  lincresunit2  42746  fllog2  42841  dignn0ldlem  42875  dignn0flhalflem1  42888  nn0sumshdiglemA  42892  nn0sumshdiglemB  42893  setrec1lem2  42914  aacllem  43029
  Copyright terms: Public domain W3C validator