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

Theorem mpancom 704
Description: An inference based on modus ponens with commutation of antecedents. (Contributed by NM, 28-Oct-2003.) (Proof shortened by Wolf Lammen, 7-Apr-2013.)
Hypotheses
Ref Expression
mpancom.1 (𝜓𝜑)
mpancom.2 ((𝜑𝜓) → 𝜒)
Assertion
Ref Expression
mpancom (𝜓𝜒)

Proof of Theorem mpancom
StepHypRef Expression
1 mpancom.1 . 2 (𝜓𝜑)
2 id 22 . 2 (𝜓𝜓)
3 mpancom.2 . 2 ((𝜑𝜓) → 𝜒)
41, 2, 3syl2anc 694 1 (𝜓𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 197  df-an 385
This theorem is referenced by:  mpan  706  spesbc  3554  xpiindi  5290  fununfun  5972  dffv2  6310  fliftcnv  6601  riotaprop  6675  elovmpt3rab1  6935  3xpexg  7003  orduniorsuc  7072  unielxp  7248  dmtpos  7409  tpossym  7429  oesuclem  7650  ercnv  7808  cnvct  8074  undom  8089  sucxpdom  8210  3xpfi  8273  pwfilem  8301  rankr1id  8763  cardnn  8827  alephnbtwn2  8933  alephsucdom  8940  cdainflem  9051  isfin4-3  9175  axcclem  9317  dmct  9384  mptct  9398  infxpidm  9422  fpwwe2lem9  9498  gchpwdom  9530  elwina  9546  elina  9547  rankcf  9637  ltexprlem4  9899  lem1  10902  ltdivp1i  10988  rpnnen1lem5  11856  rpnnen1lem5OLD  11862  eluzfz1  12386  fzpred  12427  uznfz  12461  fz0fzdiffz0  12487  fzctr  12490  flid  12649  modid0  12736  2txmodxeq0  12770  faclbnd3  13119  faclbnd4lem4  13123  bcn1  13140  hashfac  13280  repswsymballbi  13573  wrdlen2i  13732  dfrtrclrec2  13841  rtrclreclem3  13844  rtrclreclem4  13845  relexpindlem  13847  sqrtsq  14054  absrdbnd  14125  sqreulem  14143  sqreu  14144  bpoly2  14832  gcd0id  15287  lcmgcdlem  15366  lcmftp  15396  dvdsnprmd  15450  pcprod  15646  fldivp1  15648  invsym2  16470  pleval2i  17011  subrgsubm  18841  cncrng  19815  znchr  19959  mattposvs  20309  smadiadetglem2  20526  tg1  20816  cldval  20875  cldss  20881  cldopn  20883  1stcrestlem  21303  refbas  21361  refssex  21362  regr1  21601  kqreg  21602  kqnrm  21603  ufilen  21781  symgtgp  21952  elrnust  22075  psmetdmdm  22157  metuval  22401  icoopnst  22785  cnheiborlem  22800  cfilfcls  23118  eflogeq  24393  logdivlt  24412  logdifbnd  24765  harmonicbnd4  24782  basellem5  24856  bposlem7  25060  zabsle1  25066  chto1ub  25210  chpo1ub  25214  vmadivsum  25216  dchrmusum2  25228  dchrvmasum2if  25231  dchrvmasumlema  25234  dchrvmasumiflem2  25236  dchrisum0re  25247  dchrvmasumlem  25257  rplogsum  25261  mulogsumlem  25265  logdivsum  25267  selberg2lem  25284  pntrmax  25298  pntlem3  25343  pntleml  25345  pnt2  25347  usgredg2vlem2  26163  vtxdgelxnn0  26424  wlkonprop  26610  wksonproplem  26657  wwlknbp  26790  wspthnp  26799  wlklnwwlkln1  26822  clwwlkf  27010  wwlksext2clwwlkOLD  27022  erclwwlknsym  27034  erclwwlkntr  27035  clwlksfclwwlk  27049  eupth0  27192  numclwlk1lem2fo  27348  numclwlk2lem2f  27357  numclwlk2lem2fOLD  27364  numclwwlk5lem  27374  hilablo  28145  hhssabloilem  28246  mayete3i  28715  homulid2  28787  adjeu  28876  lnopeqi  28995  cnlnadjlem7  29060  adjbdlnb  29071  nmopcoadji  29088  bracnlnval  29101  elunirn2  29579  mptctf  29623  xraddge02  29649  xrge0npcan  29822  gsumle  29907  gsumvsca1  29910  gsumvsca2  29911  metidval  30061  pstmval  30066  baselsiga  30306  sigasspw  30307  ddeval1  30425  ddeval0  30426  braew  30433  derangen2  31282  subfaclim  31296  snmlff  31437  elfzm12  31695  noextendlt  31947  fnetr  32471  wl-sbal1  33476  poimirlem13  33552  poimirlem14  33553  poimirlem31  33570  poimirlem32  33571  ismblfin  33580  itg2addnclem2  33592  areacirclem2  33631  areacirc  33635  ismgmOLD  33779  ismndo2  33803  rngomndo  33864  prter3  34486  atbase  34894  llnbase  35113  lplnbase  35138  lvolbase  35182  lhpbase  35602  mzpsubmpt  37623  mzpnegmpt  37624  eliunov2  38288  iunrelexp0  38311  enmappwid  38611  uunT1  39324  nnfoctb  39527  afveu  41554  fzopredsuc  41658  fargshiftfva  41704  lindsrng01  42582
  Copyright terms: Public domain W3C validator