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

Theorem com23 83
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 40 . 2 (𝜒 → ((𝜒𝜃) → 𝜃))
31, 2syl9 74 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  84  com13  85  pm2.04  87  pm2.86d  104  expcomd  452  impancom  454  a2and  848  dedlem0b  991  3com23  1262  ad5ant13  1292  ad5ant14  1293  ad5ant15  1294  ad5ant134  1304  ad5ant135  1305  moexex  2528  ralrimdvva  2956  ceqsalt  3200  vtoclgft  3226  vtoclgftOLD  3227  reu6  3361  sbciegft  3432  reupick  3869  reusv3  4797  ralxfrd  4800  ralxfrd2  4805  pwssun  4934  wefrc  5022  ssrel  5120  ssrel2  5122  ssrelrel  5132  predpo  5601  tz7.7  5652  ordtr2  5671  onmindif  5718  unizlim  5747  funssres  5830  fv3  6101  fvmptt  6193  fveqdmss  6247  fvcofneq  6260  fmptsnd  6318  funfvima2  6375  isoini  6466  isopolem  6473  weniso  6482  f1ocnv2d  6761  limsssuc  6919  tfindsg  6929  limomss  6939  findsg  6962  funcnvuni  6989  f1oweALT  7020  bropopvvv  7119  bropfvvvvlem  7120  bropfvvvv  7121  f1o2ndf1  7149  frxp  7151  suppfnss  7184  wfr3g  7277  wfrlem12  7290  onfununi  7302  tz7.49  7404  omordi  7510  omlimcl  7522  omass  7524  oeordsuc  7538  nnmordi  7575  nnmord  7576  omabs  7591  xpdom2  7917  infensuc  8000  findcard2  8062  findcard2d  8064  findcard3  8065  frfi  8067  xpfi  8093  fsuppres  8160  dffi2  8189  elfiun  8196  ordiso2  8280  ordtypelem7  8289  suc11reg  8376  inf3lem2  8386  noinfep  8417  cantnfle  8428  cantnflem1  8446  cantnf  8450  trcl  8464  epfrs  8467  r1sdom  8497  pr2ne  8688  dfac8alem  8712  indcardi  8724  alephordi  8757  dfac12lem3  8827  pwsdompw  8886  cofsmo  8951  cfcoflem  8954  coftr  8955  isf32lem2  9036  isf32lem9  9043  axcc3  9120  domtriomlem  9124  axdc3lem2  9133  axdc3lem4  9135  zorn2lem4  9181  zorn2lem6  9183  zorn2lem7  9184  ttukeylem6  9196  uniimadom  9222  konigthlem  9246  fpwwe2lem8  9315  tskord  9458  tskcard  9459  grupr  9475  gruiin  9488  grudomon  9495  grur1a  9497  nqereu  9607  genpn0  9681  genpcd  9684  distrlem5pr  9705  psslinpr  9709  ltaddpr  9712  ltexprlem3  9716  ltexprlem6  9719  ltapr  9723  prlem936  9725  suplem1pr  9730  axpre-sup  9846  1re  9895  ltletr  9980  dedekindle  10052  lemul12a  10730  divgt0  10740  divge0  10741  lbreu  10822  sup2  10828  bndndx  11138  elnnz  11220  nzadd  11258  fzind  11307  fnn0ind  11308  uzwo  11583  eqreznegel  11606  lbzbi  11608  zmax  11617  zbtwnre  11618  irradd  11644  irrmul  11645  ledivge1le  11733  xrltletr  11823  xrub  11970  supxrunb2  11978  infmremnf  12000  iccid  12047  uzsubsubfz  12189  fzrevral  12249  elfz0fzfz0  12268  fz0fzelfz0  12269  elfzmlbp  12274  elincfzoext  12348  elfzodifsumelfzo  12356  ssfzoulel  12383  ssfzo12bi  12384  elfzonelfzo  12391  elfznelfzo  12394  elfznelfzob  12395  injresinjlem  12405  fleqceilz  12470  modaddmodup  12550  uzindi  12598  suppssfz  12611  mptnn0fsuppr  12616  le2sq2  12756  sqlecan  12788  facdiv  12891  facwordi  12893  faclbnd  12894  hashle00  13001  hashimarni  13038  hash2prd  13064  pr2pwpr  13066  fi1uzind  13080  brfi1indALT  13083  fi1uzindOLD  13086  brfi1indALTOLD  13089  swrdnd2  13231  swrdswrdlem  13257  swrdswrd  13258  ccatopth2  13269  wrd2ind  13275  reuccats1lem  13277  swrdccatin1  13280  swrdccatin12lem2a  13282  swrdccatin2  13284  swrdccatin12lem2  13286  swrdccatin12lem3  13287  swrdccat  13290  swrdccat3blem  13292  repswswrd  13328  cshwidxmod  13346  cshwidx0  13349  2cshwcshw  13368  cshwcsh2id  13371  cau3lem  13888  caubnd  13892  climrlim2  14072  rlimuni  14075  rlimcn2  14115  mulcn2  14120  rlimno1  14178  climcau  14195  climbdd  14196  caucvg  14203  modfsummod  14313  dvdsle  14816  dvdsdivcl  14822  ltoddhalfle  14869  halfleoddlt  14870  ndvdssub  14917  gcdcllem1  15005  dvdslegcd  15010  bezoutlem4  15043  dfgcd2  15047  lcmf  15130  lcmfunsnlem1  15134  lcmfunsnlem2lem1  15135  lcmfunsnlem2  15137  lcmfunsnlem  15138  lcmfdvdsb  15140  lcmfun  15142  coprmdvds1  15149  coprmdvds  15150  coprmdvdsOLD  15151  coprmdvds2  15152  divgcdcoprm0  15163  cncongr1  15165  cncongr2  15166  prmfac1  15215  pcqcl  15345  dvdsprmpweqle  15374  oddprmdvds  15391  prmpwdvds  15392  infpnlem1  15398  prmgaplem5  15543  prmgaplem6  15544  prmgaplem7  15545  cshwshashlem1  15586  cictr  16234  initoeu2lem1  16433  initoeu2  16435  clatleglb  16895  mulgaddcom  17333  mulginvcom  17334  gsmsymgrfixlem1  17616  gsmsymgreqlem2  17620  symggen  17659  psgnunilem4  17686  sylow2blem3  17806  lsmdisj2  17864  frgpnabllem1  18045  dprddisj2  18207  f1rhm0to0ALT  18510  lmodfopnelem1  18668  lssssr  18720  lss1d  18730  lspsncv0  18913  mplcoe5lem  19234  cply1mul  19431  coe1fzgsumdlem  19438  gsummoncoe1  19441  evl1gsumdlem  19487  znrrg  19678  mamufacex  19956  dmatelnd  20063  scmataddcl  20083  scmatsubcl  20084  scmatmulcl  20085  smatvscl  20091  mavmulsolcl  20118  mdetdiagid  20167  cramerlem3  20256  pmatcoe1fsupp  20267  cpmatacl  20282  cpmatmcllem  20284  mp2pm2mplem4  20375  chpscmat  20408  chfacfisf  20420  chfacfisfcpmat  20421  uniopn  20469  opnnei  20676  neindisj2  20679  restcls  20737  restntr  20738  tgcnp  20809  subbascn  20810  iscnp4  20819  lmcnp  20860  lpcls  20920  cmpsublem  20954  cmpsub  20955  tgcmp  20956  cmpcld  20957  dfcon2  20974  1stcrest  21008  2ndcdisj  21011  1stccnp  21017  comppfsc  21087  kgencn2  21112  txlm  21203  kqreglem1  21296  filin  21410  isfil2  21412  fgss2  21430  fgfil  21431  ufilmax  21463  ufileu  21475  filufint  21476  cfinufil  21484  elfm2  21504  rnelfmlem  21508  rnelfm  21509  fmfnfmlem2  21511  fmfnfmlem4  21513  flimopn  21531  fbflim2  21533  flffbas  21551  fclsnei  21575  flimfnfcls  21584  fclscmp  21586  ufilcmp  21588  fcfnei  21591  cnpfcf  21597  alexsubALTlem2  21604  alexsubALTlem3  21605  alexsubALTlem4  21606  alexsubALT  21607  ptcmplem4  21611  qustgplem  21676  tsmsres  21699  tsmsxp  21710  metss  22064  metcnp3  22096  ivthlem2  22945  ivthlem3  22946  ovoliunnul  22999  ovolicc2lem3  23011  dyadmax  23089  itg2le  23229  itgcn  23332  ellimc3  23366  lhop1  23498  dvfsumrlim  23515  fta1g  23648  fta1  23784  aalioulem3  23810  aalioulem4  23811  ulmcaulem  23869  ulmcau  23870  xrlimcnp  24412  cxploglim  24421  jensen  24432  lgsqrmodndvds  24795  gausslemma2dlem1a  24807  gausslemma2dlem2  24809  gausslemma2dlem3  24810  lgsquad2lem2  24827  2lgslem1a1  24831  2sqlem6  24865  brbtwn2  25503  ax5seglem5  25531  axcontlem4  25565  axcontlem10  25571  usgranloopv  25673  usgranloop  25674  usgra2edg  25677  usgraedg4  25682  usgra1v  25685  usgraidx2vlem2  25687  usgrafisindb0  25703  usgrafisindb1  25704  usgrares1  25705  cusgrarn  25754  cusgrares  25767  cusgrasize2inds  25771  cusgrafi  25776  sizeusglecusg  25780  usgrwlknloop  25859  1pthoncl  25888  wlkdvspthlem  25903  wlkdvspth  25904  usgra2wlkspthlem2  25914  cyclnspth  25925  fargshiftfo  25932  fargshiftfva  25933  usgrcyclnl1  25934  nvnencycllem  25937  constr3trllem2  25945  4cycl4dv  25961  wwlknimp  25981  wlkiswwlk2  25991  wwlknred  26017  wwlknext  26018  wwlknextbi  26019  wwlkextwrd  26022  wwlkextinj  26024  wwlkextproplem2  26036  wwlkextproplem3  26037  clwwlkgt0  26065  clwwlknprop  26066  clwlkisclwwlklem2a4  26078  clwlkisclwwlklem2a  26079  clwlkisclwwlklem0  26082  clwwlkf  26088  wwlkext2clwwlk  26097  clwwisshclwwlem1  26099  erclwwlkeqlen  26106  erclwwlksym  26108  clwwlknscsh  26113  erclwwlkneqlen  26118  erclwwlknsym  26120  wlklenvclwlk  26132  clwlkfclwwlk  26137  clwlkfoclwwlk  26138  el2wlkonot  26162  usg2wotspth  26177  usg2spthonot  26181  usg2spthonot0  26182  usgfiregdegfi  26204  nbhashuvtx1  26208  rusgraprop4  26237  eupatrl  26261  3vfriswmgra  26298  1to2vfriswmgra  26299  1to3vfriswmgra  26300  3cyclfrgrarn  26306  n4cyclfrgra  26311  4cyclusnfrgra  26312  frgranbnb  26313  frgrancvvdeqlemB  26331  frg2wot1  26350  frg2woteqm  26352  frg2woteq  26353  usg2spot2nb  26358  2spotmdisj  26361  usgreghash2spot  26362  frgregordn0  26363  numclwwlkovf2ex  26379  numclwlk1lem2fo  26388  numclwlk2lem2f  26396  numclwwlk8  26408  frgrareg  26410  frgraregord013  26411  frgraogt3nreg  26413  nmoub3i  26818  ipasslem5  26880  htthlem  26964  ocin  27345  spansneleq  27619  spansnss  27620  elspansn4  27622  h1datomi  27630  nmopub2tALT  27958  nmfnleub2  27975  hstel2  28268  cvnbtwn  28335  spansncv2  28342  dmdmd  28349  dmdbr3  28354  dmdbr4  28355  dmdbr5  28357  mdsl0  28359  mdexchi  28384  cvexchlem  28417  atcv1  28429  atomli  28431  atcvatlem  28434  atcvat2i  28436  chirredi  28443  mdsymlem3  28454  mdsymlem4  28455  sumdmdii  28464  sumdmdlem  28467  cdj1i  28482  ssrelf  28611  f1o3d  28619  cvxpcon  30284  mrsubccat  30475  msubvrs  30517  fundmpss  30716  dfon2lem6  30743  dfon2lem8  30745  dfon2lem9  30746  dfon2  30747  trpredrec  30788  soseq  30801  wzel  30821  wzelOLD  30822  frr3g  30829  frrlem11  30842  nodenselem5  30890  nodenselem7  30892  nodenselem8  30893  nofulllem5  30911  colinearxfr  31158  btwnconn1lem11  31180  lineintmo  31240  trer  31286  elicc3  31287  finminlem  31288  nn0prpwlem  31293  fnessref  31328  neibastop2  31332  fgmin  31341  tailfb  31348  ordcmp  31422  ee7.2aOLD  31436  bj-ceqsalt0  31863  bj-ceqsalt1  31864  isbasisrelowllem1  32175  isbasisrelowllem2  32176  relowlpssretop  32184  wl-mo3t  32333  finixpnum  32360  matunitlindflem1  32371  matunitlindflem2  32372  poimirlem26  32401  poimirlem27  32402  poimirlem29  32404  bddiblnc  32446  ftc1anc  32459  fdc  32507  heibor1lem  32574  ghomco  32656  rngoueqz  32705  unichnidl  32796  dmncan1  32841  ax12indn  33042  lshpdisj  33088  lub0N  33290  glb0N  33294  leat2  33395  hlrelat2  33503  cvrexchlem  33519  cvratlem  33521  atcvrj0  33528  cvrat2  33529  snatpsubN  33850  linepsubN  33852  pmaple  33861  pmapsub  33868  elpaddn0  33900  paddasslem5  33924  trlval2  34264  cdlemn11pre  35313  dihord2pre  35328  mapdordlem2  35740  pell1qrgap  36252  dford3lem1  36407  hbtlem5  36513  ntrneiiso  37205  sbiota1  37453  19.41rg  37583  ee223  37676  funressnfv  39654  nltle2tri  39740  el1fzopredsuc  39746  iccpartlt  39760  iccpartgt  39763  iccelpart  39769  icceuelpart  39772  iccpartnel  39774  goldbachthlem2  39794  odz2prm2pw  39811  fmtnoprmfac1  39813  fmtnofac2lem  39816  prmdvdsfmtnof1lem2  39833  2pwp1prm  39839  sfprmdvdsmersenne  39856  lighneallem3  39860  gbegt5  39981  bgoldbwt  39997  sgoldbalt  40001  bgoldbtbndlem2  40020  bgoldbtbndlem3  40021  bgoldbtbndlem4  40022  bgoldbtbnd  40023  tgblthelfgott  40027  tgoldbach  40030  tgblthelfgottOLD  40034  tgoldbachOLD  40037  lswn0  40040  pfxccatin12lem2  40085  reuccatpfxs1lem  40094  propeqop  40119  ssrelrn  40129  f1ssf1  40140  funsndifnop  40141  fundmge2nop0  40145  zm1nn  40168  fzoopth  40180  xnn0xaddcl  40208  umgrnloopv  40326  umgrnloop  40328  umgrislfupgrlem  40342  upgredgpr  40369  usgrausgrb  40394  usgrnloopvALT  40423  usgrnloopALT  40425  uhgr2edg  40430  usgredg2vlem2  40448  ushgredgedga  40451  ushgredgedgaloop  40453  nbgr0vtxlem  40572  nbusgrvtxm1  40602  uvtxanbgrvtx  40614  cusgredg  40641  cusgrres  40659  cusgrsize2inds  40664  cusgrfi  40669  fusgrregdegfi  40764  ewlkle  40802  upgrewlkle2  40803  upgr1wlkwlk  40842  upgrwlkedg  40845  uspgr2wlkeqi  40851  1wlkv0  40854  1wlklenvclwlk  40858  lfgrwlkprop  40891  lfgr1wlknloop  40893  pthdivtx  40930  2pthnloop  40932  upgrwlkdvdelem  40937  upgrspths1wlk  40939  usgr2wlkneq  40957  usgr2trlncl  40961  usgr2pthlem  40964  usgr2pth  40965  crctcsh1wlkn0lem4  41011  crctcsh1wlkn0lem5  41012  crctcsh1wlkn0  41019  1wlkiswwlks1  41059  1wlkiswwlks2  41067  1wlkiswwlksupgr2  41069  wwlksnred  41093  wwlksnext  41094  wwlksnextbi  41095  wwlksnextwrd  41098  wwlksnextinj  41100  wwlksnextproplem2  41111  wwlksnextproplem3  41112  wspthsnonn0vne  41119  2pthon3v-av  41145  wwlks2onv  41153  umgrwwlks2on  41156  elwspths2on  41158  wpthswwlks2on  41159  clwlkclwwlklem2a4  41201  clwlkclwwlklem2a  41202  clwlkclwwlklem3  41205  clwwlks1loop  41210  umgrclwwlksge2  41214  clwwlksf  41217  wwlksext2clwwlk  41226  clwwisshclwwslemlem  41228  erclwwlkseqlen  41235  erclwwlkssym  41237  clwwlksnscsh  41242  erclwwlksnsym  41249  clwlksfclwwlk  41264  upgr3v3e3cycl  41342  upgr4cycl4dv4e  41347  upgreupthi  41371  eucrctshift  41406  3vfriswmgr  41443  1to2vfriswmgr  41444  1to3vfriswmgr  41445  n4cyclfrgr  41456  4cyclusnfrgr  41457  frgrnbnb  41458  frgrncvvdeqlemB  41472  frgr2wwlk1  41489  fusgr2wsp2nb  41493  2wspmdisj  41496  fusgreghash2wsp  41497  frrusgrord0  41498  av-clwwlkextfrlem1  41504  av-extwwlkfablem2  41505  av-numclwwlkovf2ex  41512  av-numclwlk1lem2fo  41520  av-numclwlk2lem2f  41528  av-numclwwlk8  41541  av-frgrareggt1  41542  av-frgrareg  41543  av-frgraregord013  41544  av-frgraregord13  41545  av-frgraogt3nreg  41546  lmod0rng  41653  nzerooringczr  41859  ztprmneprm  41913  ply1mulgsumlem1  41963  ply1mulgsumlem2  41964  lcoel0  42006  linindslinci  42026  lindslinindimp2lem4  42039  lindslinindsimp2lem5  42040  snlindsntor  42049  ldepspr  42051  lincresunit2  42056  fllog2  42155  dignn0ldlem  42189  dignn0flhalflem1  42202  nn0sumshdiglemA  42206  nn0sumshdiglemB  42207  aacllem  42312
  Copyright terms: Public domain W3C validator