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  1268  ad5ant13  1298  ad5ant14  1299  ad5ant15  1300  ad5ant134  1310  ad5ant135  1311  moexex  2540  ralrimdvva  2970  ceqsalt  3218  vtoclgft  3244  vtoclgftOLD  3245  reu6  3382  sbciegft  3453  reupick  3893  reusv3  4846  ralxfrd  4849  ralxfrd2  4854  propeqop  4940  pwssun  4990  wefrc  5078  ssrel  5178  ssrelOLD  5179  ssrel2  5181  ssrelrel  5191  ssrelrn  5285  predpo  5667  tz7.7  5718  ordtr2  5737  onmindif  5784  unizlim  5813  funssres  5898  f1ssf1  6135  fv3  6173  fvmptt  6266  fveqdmss  6320  fvcofneq  6333  funsndifnop  6381  fmptsnd  6400  funfvima2  6458  isoini  6553  isopolem  6560  weniso  6569  f1ocnv2d  6851  limsssuc  7012  tfindsg  7022  limomss  7032  findsg  7055  funcnvuni  7081  f1oweALT  7112  bropopvvv  7215  bropfvvvvlem  7216  bropfvvvv  7217  f1o2ndf1  7245  frxp  7247  suppfnss  7280  wfr3g  7373  wfrlem12  7386  onfununi  7398  tz7.49  7500  omordi  7606  omlimcl  7618  omass  7620  oeordsuc  7634  nnmordi  7671  nnmord  7672  omabs  7687  xpdom2  8015  infensuc  8098  findcard2  8160  findcard2d  8162  findcard3  8163  frfi  8165  xpfi  8191  fsuppres  8260  dffi2  8289  elfiun  8296  ordiso2  8380  ordtypelem7  8389  suc11reg  8476  inf3lem2  8486  noinfep  8517  cantnfle  8528  cantnflem1  8546  cantnf  8550  trcl  8564  epfrs  8567  r1sdom  8597  pr2ne  8788  dfac8alem  8812  indcardi  8824  alephordi  8857  dfac12lem3  8927  pwsdompw  8986  cofsmo  9051  cfcoflem  9054  coftr  9055  isf32lem2  9136  isf32lem9  9143  axcc3  9220  domtriomlem  9224  axdc3lem2  9233  axdc3lem4  9235  zorn2lem4  9281  zorn2lem6  9283  zorn2lem7  9284  ttukeylem6  9296  uniimadom  9326  konigthlem  9350  fpwwe2lem8  9419  tskord  9562  tskcard  9563  grupr  9579  gruiin  9592  grudomon  9599  grur1a  9601  nqereu  9711  genpn0  9785  genpcd  9788  distrlem5pr  9809  psslinpr  9813  ltaddpr  9816  ltexprlem3  9820  ltexprlem6  9823  ltapr  9827  prlem936  9829  suplem1pr  9834  axpre-sup  9950  1re  9999  ltletr  10089  dedekindle  10161  lemul12a  10841  divgt0  10851  divge0  10852  lbreu  10933  sup2  10939  bndndx  11251  elnnz  11347  nzadd  11385  fzind  11435  fnn0ind  11436  uzwo  11711  eqreznegel  11734  lbzbi  11736  zmax  11745  zbtwnre  11746  irradd  11772  irrmul  11773  ledivge1le  11861  xrltletr  11948  xnn0xaddcl  12025  xrub  12101  supxrunb2  12109  infmremnf  12131  iccid  12178  uzsubsubfz  12321  fzrevral  12382  elfz0fzfz0  12401  fz0fzelfz0  12402  elfzmlbp  12407  elincfzoext  12482  elfzodifsumelfzo  12490  ssfzoulel  12519  ssfzo12bi  12520  elfzonelfzo  12527  elfznelfzo  12530  elfznelfzob  12531  injresinjlem  12544  fleqceilz  12609  modaddmodup  12689  uzindi  12737  suppssfz  12750  mptnn0fsuppr  12755  le2sq2  12895  sqlecan  12927  facdiv  13030  facwordi  13032  faclbnd  13033  hashimarni  13182  hash2prd  13211  hashle2pr  13213  pr2pwpr  13215  fundmge2nop0  13229  fi1uzind  13234  brfi1indALT  13237  fi1uzindOLD  13240  brfi1indALTOLD  13243  swrdnd2  13387  swrdswrdlem  13413  swrdswrd  13414  ccatopth2  13425  wrd2ind  13431  reuccats1lem  13433  swrdccatin1  13436  swrdccatin12lem2a  13438  swrdccatin2  13440  swrdccatin12lem2  13442  swrdccatin12lem3  13443  swrdccat  13446  swrdccat3blem  13448  repswswrd  13484  cshwidxmod  13502  cshwidx0  13505  2cshwcshw  13524  cshwcsh2id  13527  cau3lem  14044  caubnd  14048  climrlim2  14228  rlimuni  14231  rlimcn2  14271  mulcn2  14276  rlimno1  14334  climcau  14351  climbdd  14352  caucvg  14359  modfsummod  14472  dvdsle  14975  dvdsdivcl  14981  ltoddhalfle  15028  halfleoddlt  15029  ndvdssub  15076  gcdcllem1  15164  dvdslegcd  15169  bezoutlem4  15202  dfgcd2  15206  lcmf  15289  lcmfunsnlem1  15293  lcmfunsnlem2lem1  15294  lcmfunsnlem2  15296  lcmfunsnlem  15297  lcmfdvdsb  15299  lcmfun  15301  coprmdvds1  15308  coprmdvds  15309  coprmdvdsOLD  15310  coprmdvds2  15311  divgcdcoprm0  15322  cncongr1  15324  cncongr2  15325  prmfac1  15374  pcqcl  15504  dvdsprmpweqle  15533  oddprmdvds  15550  prmpwdvds  15551  infpnlem1  15557  prmgaplem5  15702  prmgaplem6  15703  prmgaplem7  15704  cshwshashlem1  15745  cictr  16405  initoeu2lem1  16604  initoeu2  16606  clatleglb  17066  mulgaddcom  17504  mulginvcom  17505  gsmsymgrfixlem1  17787  gsmsymgreqlem2  17791  symggen  17830  psgnunilem4  17857  sylow2blem3  17977  lsmdisj2  18035  frgpnabllem1  18216  dprddisj2  18378  f1rhm0to0ALT  18681  lmodfopnelem1  18839  lssssr  18893  lss1d  18903  lspsncv0  19086  mplcoe5lem  19407  cply1mul  19604  coe1fzgsumdlem  19611  gsummoncoe1  19614  evl1gsumdlem  19660  znrrg  19854  mamufacex  20135  dmatelnd  20242  scmataddcl  20262  scmatsubcl  20263  scmatmulcl  20264  smatvscl  20270  mavmulsolcl  20297  mdetdiagid  20346  cramerlem3  20435  pmatcoe1fsupp  20446  cpmatacl  20461  cpmatmcllem  20463  mp2pm2mplem4  20554  chpscmat  20587  chfacfisf  20599  chfacfisfcpmat  20600  uniopn  20642  opnnei  20864  neindisj2  20867  restcls  20925  restntr  20926  tgcnp  20997  subbascn  20998  iscnp4  21007  lmcnp  21048  lpcls  21108  cmpsublem  21142  cmpsub  21143  tgcmp  21144  cmpcld  21145  dfconn2  21162  1stcrest  21196  2ndcdisj  21199  1stccnp  21205  comppfsc  21275  kgencn2  21300  txlm  21391  kqreglem1  21484  filin  21598  isfil2  21600  fgss2  21618  fgfil  21619  ufilmax  21651  ufileu  21663  filufint  21664  cfinufil  21672  elfm2  21692  rnelfmlem  21696  rnelfm  21697  fmfnfmlem2  21699  fmfnfmlem4  21701  flimopn  21719  fbflim2  21721  flffbas  21739  fclsnei  21763  flimfnfcls  21772  fclscmp  21774  ufilcmp  21776  fcfnei  21779  cnpfcf  21785  alexsubALTlem2  21792  alexsubALTlem3  21793  alexsubALTlem4  21794  alexsubALT  21795  ptcmplem4  21799  qustgplem  21864  tsmsres  21887  tsmsxp  21898  metss  22253  metcnp3  22285  ivthlem2  23161  ivthlem3  23162  ovoliunnul  23215  ovolicc2lem3  23227  dyadmax  23306  itg2le  23446  itgcn  23549  ellimc3  23583  lhop1  23715  dvfsumrlim  23732  fta1g  23865  fta1  24001  aalioulem3  24027  aalioulem4  24028  ulmcaulem  24086  ulmcau  24087  xrlimcnp  24629  cxploglim  24638  jensen  24649  lgsqrmodndvds  25012  gausslemma2dlem1a  25024  gausslemma2dlem2  25026  gausslemma2dlem3  25027  lgsquad2lem2  25044  2lgslem1a1  25048  2sqlem6  25082  brbtwn2  25719  ax5seglem5  25747  axcontlem4  25781  axcontlem10  25787  umgrnloopv  25930  umgrnloop  25932  umgrislfupgrlem  25946  upgredgpr  25966  usgrausgrb  25991  usgrnloopvALT  26020  usgrnloopALT  26022  uhgr2edg  26027  usgredg2vlem2  26045  ushgredgedg  26048  ushgredgedgloop  26050  nbgr0vtxlem  26172  nbusgrvtxm1  26202  uvtxanbgrvtx  26214  cusgredg  26241  cusgrres  26265  cusgrsize2inds  26270  cusgrfi  26275  fusgrregdegfi  26369  ewlkle  26405  upgrewlkle2  26406  uspgr2wlkeqi  26447  wlkv0  26450  wlklenvclwlk  26454  lfgrwlkprop  26487  lfgrwlknloop  26489  pthdivtx  26528  2pthnloop  26530  upgrwlkdvdelem  26535  upgrspthswlk  26537  usgr2wlkneq  26555  usgr2trlncl  26559  usgr2pthlem  26562  usgr2pth  26563  uspgrn2crct  26603  crctcshwlkn0lem4  26608  crctcshwlkn0lem5  26609  crctcshwlkn0  26616  wlkiswwlks1  26656  wlkiswwlks2  26664  wlkiswwlksupgr2  26666  wwlksnred  26690  wwlksnext  26691  wwlksnextbi  26692  wwlksnextwrd  26695  wwlksnextinj  26697  wwlksnextproplem2  26708  wwlksnextproplem3  26709  wspthsnonn0vne  26716  2pthon3v  26742  wwlks2onv  26750  umgrwwlks2on  26753  elwspths2on  26755  wpthswwlks2on  26756  clwlkclwwlklem2a4  26799  clwlkclwwlklem2a  26800  clwlkclwwlklem3  26803  clwwlks1loop  26808  umgrclwwlksge2  26812  clwwlksf  26815  wwlksext2clwwlk  26824  clwwisshclwwslemlem  26826  erclwwlkseqlen  26833  erclwwlkssym  26835  clwwlksnscsh  26840  erclwwlksnsym  26847  clwlksfclwwlk  26862  upgr3v3e3cycl  26940  upgr4cycl4dv4e  26945  eucrctshift  27003  3vfriswmgr  27040  1to2vfriswmgr  27041  1to3vfriswmgr  27042  n4cyclfrgr  27053  4cyclusnfrgr  27054  frgrnbnb  27055  frgrncvvdeqlemB  27069  frgr2wwlk1  27086  fusgr2wsp2nb  27090  2wspmdisj  27093  fusgreghash2wsp  27094  frrusgrord0  27095  clwwlkextfrlem1  27101  extwwlkfablem2  27102  numclwwlkovf2ex  27109  numclwlk1lem2fo  27117  numclwlk2lem2f  27125  numclwwlk8  27138  frgrreggt1  27139  frgrreg  27140  frgrregord013  27141  frgrregord13  27142  frgrogt3nreg  27143  eulplig  27225  nmoub3i  27516  ipasslem5  27578  htthlem  27662  ocin  28043  spansneleq  28317  spansnss  28318  elspansn4  28320  h1datomi  28328  nmopub2tALT  28656  nmfnleub2  28673  hstel2  28966  cvnbtwn  29033  spansncv2  29040  dmdmd  29047  dmdbr3  29052  dmdbr4  29053  dmdbr5  29055  mdsl0  29057  mdexchi  29082  cvexchlem  29115  atcv1  29127  atomli  29129  atcvatlem  29132  atcvat2i  29134  chirredi  29141  mdsymlem3  29152  mdsymlem4  29153  sumdmdii  29162  sumdmdlem  29165  cdj1i  29180  ssrelf  29309  f1o3d  29316  cvxpconn  30985  mrsubccat  31176  msubvrs  31218  fundmpss  31421  dfon2lem6  31447  dfon2lem8  31449  dfon2lem9  31450  dfon2  31451  trpredrec  31492  soseq  31505  wzel  31525  wzelOLD  31526  frr3g  31533  frrlem11  31546  nodenselem5  31601  nodenselem7  31603  nodenselem8  31604  nosepdmlem  31620  colinearxfr  31877  btwnconn1lem11  31899  lineintmo  31959  trer  32005  elicc3  32006  finminlem  32007  nn0prpwlem  32012  fnessref  32047  neibastop2  32051  fgmin  32060  tailfb  32067  ordcmp  32141  ee7.2aOLD  32155  bj-ceqsalt0  32573  bj-ceqsalt1  32574  isbasisrelowllem1  32874  isbasisrelowllem2  32875  relowlpssretop  32883  wl-mo3t  33029  finixpnum  33065  matunitlindflem1  33076  matunitlindflem2  33077  poimirlem26  33106  poimirlem27  33107  poimirlem29  33109  bddiblnc  33151  ftc1anc  33164  fdc  33212  heibor1lem  33279  ghomco  33361  rngoueqz  33410  unichnidl  33501  dmncan1  33546  ax12indn  33747  lshpdisj  33793  lub0N  33995  glb0N  33999  leat2  34100  hlrelat2  34208  cvrexchlem  34224  cvratlem  34226  atcvrj0  34233  cvrat2  34234  snatpsubN  34555  linepsubN  34557  pmaple  34566  pmapsub  34573  elpaddn0  34605  paddasslem5  34629  trlval2  34969  cdlemn11pre  36018  dihord2pre  36033  mapdordlem2  36445  pell1qrgap  36957  dford3lem1  37112  hbtlem5  37218  ntrneiiso  37910  sbiota1  38156  19.41rg  38287  ee223  38380  funressnfv  40542  zm1nn  40643  nltle2tri  40650  el1fzopredsuc  40662  fzoopth  40664  iccpartlt  40688  iccpartgt  40691  iccelpart  40697  icceuelpart  40700  iccpartnel  40702  fargshiftfo  40706  fargshiftfva  40707  lswn0  40708  pfxccatin12lem2  40753  reuccatpfxs1lem  40762  goldbachthlem2  40787  odz2prm2pw  40804  fmtnoprmfac1  40806  fmtnofac2lem  40809  prmdvdsfmtnof1lem2  40826  2pwp1prm  40832  sfprmdvdsmersenne  40849  lighneallem3  40853  gbegt5  40974  bgoldbwt  40990  sgoldbalt  40994  bgoldbtbndlem2  41013  bgoldbtbndlem3  41014  bgoldbtbndlem4  41015  bgoldbtbnd  41016  tgblthelfgott  41020  tgoldbach  41023  tgblthelfgottOLD  41027  tgoldbachOLD  41030  upgrwlkupwlk  41039  prsprel  41055  sprsymrelfolem2  41061  sprsymrelfo  41065  lmod0rng  41186  nzerooringczr  41390  ztprmneprm  41443  ply1mulgsumlem1  41492  ply1mulgsumlem2  41493  lcoel0  41535  linindslinci  41555  lindslinindimp2lem4  41568  lindslinindsimp2lem5  41569  snlindsntor  41578  ldepspr  41580  lincresunit2  41585  fllog2  41684  dignn0ldlem  41718  dignn0flhalflem1  41731  nn0sumshdiglemA  41735  nn0sumshdiglemB  41736  setrec1lem2  41758  aacllem  41880
  Copyright terms: Public domain W3C validator