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  454  impancom  456  a2and  852  dedlem0b  1000  3com23  1269  ad5ant13  1299  ad5ant14  1300  ad5ant15  1301  ad5ant134  1311  ad5ant135  1312  moexex  2539  ralrimdvva  2971  ceqsalt  3223  vtoclgft  3249  vtoclgftOLD  3250  reu6  3389  sbciegft  3460  reupick  3903  reusv3  4867  ralxfrd  4870  ralxfrd2  4875  propeqop  4960  pwssun  5010  wefrc  5098  ssrel  5197  ssrelOLD  5198  ssrel2  5200  ssrelrel  5210  ssrelrn  5304  predpo  5686  tz7.7  5737  ordtr2  5756  onmindif  5803  unizlim  5832  funssres  5918  f1ssf1  6155  fv3  6193  fvmptt  6286  fveqdmss  6340  fvcofneq  6353  funsndifnop  6401  fmptsnd  6420  funfvima2  6478  isoini  6573  isopolem  6580  weniso  6589  f1ocnv2d  6871  limsssuc  7035  tfindsg  7045  limomss  7055  findsg  7078  funcnvuni  7104  f1oweALT  7137  bropopvvv  7240  bropfvvvvlem  7241  bropfvvvv  7242  f1o2ndf1  7270  frxp  7272  suppfnss  7305  wfr3g  7398  wfrlem12  7411  onfununi  7423  tz7.49  7525  omordi  7631  omlimcl  7643  omass  7645  oeordsuc  7659  nnmordi  7696  nnmord  7697  omabs  7712  xpdom2  8040  infensuc  8123  findcard2  8185  findcard2d  8187  findcard3  8188  frfi  8190  xpfi  8216  fsuppres  8285  dffi2  8314  elfiun  8321  ordiso2  8405  ordtypelem7  8414  suc11reg  8501  inf3lem2  8511  noinfep  8542  cantnfle  8553  cantnflem1  8571  cantnf  8575  trcl  8589  epfrs  8592  r1sdom  8622  pr2ne  8813  dfac8alem  8837  indcardi  8849  alephordi  8882  dfac12lem3  8952  pwsdompw  9011  cofsmo  9076  cfcoflem  9079  coftr  9080  isf32lem2  9161  isf32lem9  9168  axcc3  9245  domtriomlem  9249  axdc3lem2  9258  axdc3lem4  9260  zorn2lem4  9306  zorn2lem6  9308  zorn2lem7  9309  ttukeylem6  9321  uniimadom  9351  konigthlem  9375  fpwwe2lem8  9444  tskord  9587  tskcard  9588  grupr  9604  gruiin  9617  grudomon  9624  grur1a  9626  nqereu  9736  genpn0  9810  genpcd  9813  distrlem5pr  9834  psslinpr  9838  ltaddpr  9841  ltexprlem3  9845  ltexprlem6  9848  ltapr  9852  prlem936  9854  suplem1pr  9859  axpre-sup  9975  1re  10024  ltletr  10114  dedekindle  10186  lemul12a  10866  divgt0  10876  divge0  10877  lbreu  10958  sup2  10964  bndndx  11276  elnnz  11372  nzadd  11410  fzind  11460  fnn0ind  11461  uzwo  11736  eqreznegel  11759  lbzbi  11761  zmax  11770  zbtwnre  11771  irradd  11797  irrmul  11798  ledivge1le  11886  xrltletr  11973  xnn0xaddcl  12051  xrub  12127  supxrunb2  12135  infmremnf  12158  iccid  12205  uzsubsubfz  12348  fzrevral  12409  elfz0fzfz0  12428  fz0fzelfz0  12429  elfzmlbp  12434  elincfzoext  12509  elfzodifsumelfzo  12517  ssfzoulel  12546  ssfzo12bi  12547  elfzonelfzo  12554  elfznelfzo  12557  elfznelfzob  12558  injresinjlem  12571  fleqceilz  12636  modaddmodup  12716  uzindi  12764  suppssfz  12777  mptnn0fsuppr  12782  le2sq2  12922  sqlecan  12954  facdiv  13057  facwordi  13059  faclbnd  13060  hashimarni  13211  hash2prd  13240  hashle2pr  13242  pr2pwpr  13244  fundmge2nop0  13257  fi1uzind  13262  brfi1indALT  13265  fi1uzindOLD  13268  brfi1indALTOLD  13271  swrdnd2  13415  swrdswrdlem  13441  swrdswrd  13442  ccatopth2  13453  wrd2ind  13459  reuccats1lem  13461  swrdccatin1  13464  swrdccatin12lem2a  13466  swrdccatin2  13468  swrdccatin12lem2  13470  swrdccatin12lem3  13471  swrdccat  13474  swrdccat3blem  13476  repswswrd  13512  cshwidxmod  13530  cshwidx0  13533  2cshwcshw  13552  cshwcsh2id  13555  cau3lem  14075  caubnd  14079  climrlim2  14259  rlimuni  14262  rlimcn2  14302  mulcn2  14307  rlimno1  14365  climcau  14382  climbdd  14383  caucvg  14390  modfsummod  14507  dvdsle  15013  dvdsdivcl  15019  ltoddhalfle  15066  halfleoddlt  15067  ndvdssub  15114  gcdcllem1  15202  dvdslegcd  15207  bezoutlem4  15240  dfgcd2  15244  lcmf  15327  lcmfunsnlem1  15331  lcmfunsnlem2lem1  15332  lcmfunsnlem2  15334  lcmfunsnlem  15335  lcmfdvdsb  15337  lcmfun  15339  coprmdvds1  15346  coprmdvds  15347  coprmdvdsOLD  15348  coprmdvds2  15349  divgcdcoprm0  15360  cncongr1  15362  cncongr2  15363  prmfac1  15412  pcqcl  15542  dvdsprmpweqle  15571  oddprmdvds  15588  prmpwdvds  15589  infpnlem1  15595  prmgaplem5  15740  prmgaplem6  15741  prmgaplem7  15742  cshwshashlem1  15783  cictr  16446  initoeu2lem1  16645  initoeu2  16647  clatleglb  17107  mulgaddcom  17545  mulginvcom  17546  gsmsymgrfixlem1  17828  gsmsymgreqlem2  17832  symggen  17871  psgnunilem4  17898  sylow2blem3  18018  lsmdisj2  18076  frgpnabllem1  18257  dprddisj2  18419  f1rhm0to0ALT  18722  lmodfopnelem1  18880  lssssr  18934  lss1d  18944  lspsncv0  19127  mplcoe5lem  19448  cply1mul  19645  coe1fzgsumdlem  19652  gsummoncoe1  19655  evl1gsumdlem  19701  znrrg  19895  mamufacex  20176  dmatelnd  20283  scmataddcl  20303  scmatsubcl  20304  scmatmulcl  20305  smatvscl  20311  mavmulsolcl  20338  mdetdiagid  20387  cramerlem3  20476  pmatcoe1fsupp  20487  cpmatacl  20502  cpmatmcllem  20504  mp2pm2mplem4  20595  chpscmat  20628  chfacfisf  20640  chfacfisfcpmat  20641  uniopn  20683  opnnei  20905  neindisj2  20908  restcls  20966  restntr  20967  tgcnp  21038  subbascn  21039  iscnp4  21048  lmcnp  21089  lpcls  21149  cmpsublem  21183  cmpsub  21184  tgcmp  21185  cmpcld  21186  dfconn2  21203  1stcrest  21237  2ndcdisj  21240  1stccnp  21246  comppfsc  21316  kgencn2  21341  txlm  21432  kqreglem1  21525  filin  21639  isfil2  21641  fgss2  21659  fgfil  21660  ufilmax  21692  ufileu  21704  filufint  21705  cfinufil  21713  elfm2  21733  rnelfmlem  21737  rnelfm  21738  fmfnfmlem2  21740  fmfnfmlem4  21742  flimopn  21760  fbflim2  21762  flffbas  21780  fclsnei  21804  flimfnfcls  21813  fclscmp  21815  ufilcmp  21817  fcfnei  21820  cnpfcf  21826  alexsubALTlem2  21833  alexsubALTlem3  21834  alexsubALTlem4  21835  alexsubALT  21836  ptcmplem4  21840  qustgplem  21905  tsmsres  21928  tsmsxp  21939  metss  22294  metcnp3  22326  ivthlem2  23202  ivthlem3  23203  ovoliunnul  23256  ovolicc2lem3  23268  dyadmax  23347  itg2le  23487  itgcn  23590  ellimc3  23624  lhop1  23758  dvfsumrlim  23775  fta1g  23908  fta1  24044  aalioulem3  24070  aalioulem4  24071  ulmcaulem  24129  ulmcau  24130  xrlimcnp  24676  cxploglim  24685  jensen  24696  lgsqrmodndvds  25059  gausslemma2dlem1a  25071  gausslemma2dlem2  25073  gausslemma2dlem3  25074  lgsquad2lem2  25091  2lgslem1a1  25095  2sqlem6  25129  brbtwn2  25766  ax5seglem5  25794  axcontlem4  25828  axcontlem10  25834  umgrnloopv  25982  umgrnloop  25984  umgrislfupgrlem  25998  upgredgpr  26018  numedglnl  26020  usgrausgrb  26045  usgrnloopvALT  26074  usgrnloopALT  26076  uhgr2edg  26081  usgredg2vlem2  26099  ushgredgedg  26102  ushgredgedgloop  26104  upgrreslem  26177  umgrreslem  26178  nbgr0vtxlem  26232  nbusgrvtxm1  26262  uvtxanbgrvtx  26274  cusgredg  26301  cusgrres  26325  cusgrsize2inds  26330  cusgrfi  26335  fusgrregdegfi  26446  ewlkle  26482  upgrewlkle2  26483  uspgr2wlkeqi  26525  wlkv0  26528  wlklenvclwlk  26532  lfgrwlkprop  26565  lfgrwlknloop  26567  pthdivtx  26606  2pthnloop  26608  upgrwlkdvdelem  26613  upgrspthswlk  26615  usgr2wlkneq  26633  usgr2trlncl  26637  usgr2pthlem  26640  usgr2pth  26641  uspgrn2crct  26681  crctcshwlkn0lem4  26686  crctcshwlkn0lem5  26687  crctcshwlkn0  26694  wlkiswwlks1  26734  wlkiswwlks2  26742  wlkiswwlksupgr2  26744  wwlksnred  26768  wwlksnext  26769  wwlksnextbi  26770  wwlksnextwrd  26773  wwlksnextinj  26775  wwlksnextproplem2  26786  wwlksnextproplem3  26787  wspthsnonn0vne  26794  2pthon3v  26820  wwlks2onv  26828  umgrwwlks2on  26831  elwspths2on  26834  wpthswwlks2on  26835  clwlkclwwlklem2a4  26879  clwlkclwwlklem2a  26880  clwlkclwwlklem3  26883  clwwlks1loop  26888  umgrclwwlksge2  26892  clwwlksf  26895  wwlksext2clwwlk  26904  clwwisshclwwslemlem  26906  erclwwlkseqlen  26913  erclwwlkssym  26915  clwwlksnscsh  26920  erclwwlksnsym  26927  clwlksfclwwlk  26942  upgr3v3e3cycl  27020  upgr4cycl4dv4e  27025  eucrctshift  27083  3vfriswmgr  27122  1to2vfriswmgr  27123  1to3vfriswmgr  27124  n4cyclfrgr  27135  4cyclusnfrgr  27136  frgrnbnb  27137  frgrncvvdeqlem8  27150  frgrwopreg  27159  frgr2wwlk1  27167  frgr2wwlkeqm  27169  clwwlkextfrlem1  27183  extwwlkfablem2  27184  numclwwlkovf2ex  27191  numclwlk1lem2fo  27199  numclwlk2lem2f  27207  numclwwlk8  27220  frgrreggt1  27221  frgrreg  27222  frgrregord013  27223  frgrregord13  27224  frgrogt3nreg  27225  eulplig  27307  nmoub3i  27598  ipasslem5  27660  htthlem  27744  ocin  28125  spansneleq  28399  spansnss  28400  elspansn4  28402  h1datomi  28410  nmopub2tALT  28738  nmfnleub2  28755  hstel2  29048  cvnbtwn  29115  spansncv2  29122  dmdmd  29129  dmdbr3  29134  dmdbr4  29135  dmdbr5  29137  mdsl0  29139  mdexchi  29164  cvexchlem  29197  atcv1  29209  atomli  29211  atcvatlem  29214  atcvat2i  29216  chirredi  29223  mdsymlem3  29234  mdsymlem4  29235  sumdmdii  29244  sumdmdlem  29247  cdj1i  29262  ssrelf  29397  f1o3d  29404  cvxpconn  31198  mrsubccat  31389  msubvrs  31431  fundmpss  31640  dfon2lem6  31667  dfon2lem8  31669  dfon2lem9  31670  dfon2  31671  trpredrec  31712  soseq  31725  wzel  31745  wzelOLD  31746  frr3g  31753  frrlem11  31766  nosepdmlem  31807  nodenselem8  31815  colinearxfr  32157  btwnconn1lem11  32179  lineintmo  32239  trer  32285  elicc3  32286  finminlem  32287  nn0prpwlem  32292  fnessref  32327  neibastop2  32331  fgmin  32340  tailfb  32347  ordcmp  32421  ee7.2aOLD  32435  bj-ceqsalt0  32848  bj-ceqsalt1  32849  isbasisrelowllem1  33174  isbasisrelowllem2  33175  relowlpssretop  33183  wl-mo3t  33329  finixpnum  33365  matunitlindflem1  33376  matunitlindflem2  33377  poimirlem26  33406  poimirlem27  33407  poimirlem29  33409  bddiblnc  33451  ftc1anc  33464  fdc  33512  heibor1lem  33579  ghomco  33661  rngoueqz  33710  unichnidl  33801  dmncan1  33846  ax12indn  34047  lshpdisj  34093  lub0N  34295  glb0N  34299  leat2  34400  hlrelat2  34508  cvrexchlem  34524  cvratlem  34526  atcvrj0  34533  cvrat2  34534  snatpsubN  34855  linepsubN  34857  pmaple  34866  pmapsub  34873  elpaddn0  34905  paddasslem5  34929  trlval2  35269  cdlemn11pre  36318  dihord2pre  36333  mapdordlem2  36745  pell1qrgap  37257  dford3lem1  37412  hbtlem5  37517  ntrneiiso  38209  sbiota1  38455  19.41rg  38586  ee223  38679  funressnfv  40971  zm1nn  41079  nltle2tri  41086  el1fzopredsuc  41098  fzoopth  41100  iccpartlt  41124  iccpartgt  41127  iccelpart  41133  icceuelpart  41136  iccpartnel  41138  fargshiftfo  41142  fargshiftfva  41143  lswn0  41144  pfxccatin12lem2  41189  reuccatpfxs1lem  41198  goldbachthlem2  41223  odz2prm2pw  41240  fmtnoprmfac1  41242  fmtnofac2lem  41245  prmdvdsfmtnof1lem2  41262  2pwp1prm  41268  sfprmdvdsmersenne  41285  lighneallem3  41289  even3prm2  41393  gbegt5  41414  sbgoldbwt  41430  sbgoldbalt  41434  sbgoldbm  41437  bgoldbtbndlem2  41459  bgoldbtbndlem3  41460  bgoldbtbndlem4  41461  bgoldbtbnd  41462  tgblthelfgott  41468  tgoldbach  41470  tgblthelfgottOLD  41474  tgoldbachOLD  41477  upgrwlkupwlk  41486  prsprel  41502  sprsymrelfolem2  41508  sprsymrelfo  41512  lmod0rng  41633  nzerooringczr  41837  ztprmneprm  41890  ply1mulgsumlem1  41939  ply1mulgsumlem2  41940  lcoel0  41982  linindslinci  42002  lindslinindimp2lem4  42015  lindslinindsimp2lem5  42016  snlindsntor  42025  ldepspr  42027  lincresunit2  42032  fllog2  42127  dignn0ldlem  42161  dignn0flhalflem1  42174  nn0sumshdiglemA  42178  nn0sumshdiglemB  42179  setrec1lem2  42200  aacllem  42312
  Copyright terms: Public domain W3C validator