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

Theorem mpancom 700
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 691 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 196  df-an 385
This theorem is referenced by:  mpan  702  spesbc  3487  xpiindi  5179  fununfun  5848  dffv2  6181  fliftcnv  6461  riotaprop  6534  elovmpt3rab1  6791  3xpexg  6859  orduniorsuc  6922  unielxp  7095  dmtpos  7251  tpossym  7271  oesuclem  7492  ercnv  7650  undom  7933  sucxpdom  8054  3xpfi  8117  pwfilem  8143  rankr1id  8608  cardnn  8672  alephnbtwn2  8778  alephsucdom  8785  cdainflem  8896  isfin4-3  9020  axcclem  9162  infxpidm  9263  fpwwe2lem9  9339  gchpwdom  9371  elwina  9387  elina  9388  rankcf  9478  ltexprlem4  9740  lem1  10743  ltdivp1i  10829  rpnnen1lem5  11694  rpnnen1lem5OLD  11700  eluzfz1  12219  fzpred  12259  uznfz  12292  fz0fzdiffz0  12317  fzctr  12320  flid  12471  modid0  12558  2txmodxeq0  12592  faclbnd3  12941  faclbnd4lem4  12945  bcn1  12962  hashfac  13099  repswsymballbi  13378  wrdlen2i  13534  dfrtrclrec2  13645  rtrclreclem3  13648  rtrclreclem4  13649  relexpindlem  13651  sqrtsq  13858  absrdbnd  13929  sqreulem  13947  sqreu  13948  bpoly2  14627  gcd0id  15078  lcmgcdlem  15157  lcmftp  15187  dvdsnprmd  15241  pcprod  15437  fldivp1  15439  invsym2  16246  pleval2i  16787  subrgsubm  18616  cncrng  19586  znchr  19730  mattposvs  20080  smadiadetglem2  20297  tg1  20579  cldval  20637  cldss  20643  cldopn  20645  1stcrestlem  21065  refbas  21123  refssex  21124  regr1  21363  kqreg  21364  kqnrm  21365  ufilen  21544  symgtgp  21715  elrnust  21838  psmetdmdm  21920  metuval  22164  icoopnst  22546  cnheiborlem  22561  cfilfcls  22880  eflogeq  24152  logdivlt  24171  logdifbnd  24520  harmonicbnd4  24537  basellem5  24611  bposlem7  24815  zabsle1  24821  chto1ub  24965  chpo1ub  24969  vmadivsum  24971  dchrmusum2  24983  dchrvmasum2if  24986  dchrvmasumlema  24989  dchrvmasumiflem2  24991  dchrisum0re  25002  dchrvmasumlem  25012  rplogsum  25016  mulogsumlem  25020  logdivsum  25022  selberg2lem  25039  pntrmax  25053  pntlem3  25098  pntleml  25100  pnt2  25102  usgraidx2vlem2  25921  nbcusgra  25992  uvtxnbgravtx  26023  cusgrauvtxb  26024  wlkbprop  26051  wlkonprop  26063  trlonprop  26072  pthonprop  26107  spthonprp  26115  usgra2adedgspthlem1  26139  usgra2adedgwlk  26142  cyclispthon  26161  fargshiftfva  26167  constr3lem4  26175  constr3trllem2  26179  4cycl4dv  26195  wlklniswwlkn1  26227  clwlkiswlk  26285  clwwlkf  26322  wwlkext2clwwlk  26331  erclwwlknsym  26354  erclwwlkntr  26355  clwlkfclwwlk  26371  eupatrl  26495  frgra1v  26525  frgrancvvdeqlem3  26559  numclwlk1lem2fo  26622  numclwlk2lem2f  26630  numclwwlk5lem  26638  hilablo  27401  hhssabloilem  27502  mayete3i  27971  homulid2  28043  adjeu  28132  lnopeqi  28251  cnlnadjlem7  28316  adjbdlnb  28327  nmopcoadji  28344  bracnlnval  28357  elunirn2  28831  dmct  28877  cnvct  28878  mptct  28880  mptctf  28883  xraddge02  28911  xrge0npcan  29025  gsumle  29110  gsumvsca1  29113  gsumvsca2  29114  metidval  29261  pstmval  29266  baselsiga  29505  sigasspw  29506  ddeval1  29624  ddeval0  29625  braew  29632  derangen2  30410  subfaclim  30424  snmlff  30565  elfzm12  30823  fnetr  31516  wl-sbal1  32525  poimirlem13  32592  poimirlem14  32593  poimirlem31  32610  poimirlem32  32611  ismblfin  32620  itg2addnclem2  32632  areacirclem2  32671  areacirc  32675  ismgmOLD  32819  ismndo2  32843  rngomndo  32904  prter3  33185  atbase  33594  llnbase  33813  lplnbase  33838  lvolbase  33882  lhpbase  34302  mzpsubmpt  36324  mzpnegmpt  36325  eliunov2  36990  iunrelexp0  37013  enmappwid  37314  uunT1  38028  nnfoctb  38238  afveu  39882  fzopredsuc  39946  usgredg2vlem2  40453  vtxdgelxnn0  40687  wlkOnprop  40866  1wlksonproplem  40912  wwlknbp  41044  wspthnp  41048  1wlklnwwlkln1  41065  clwwlknbp0  41192  clwwlksf  41222  wwlksext2clwwlk  41231  erclwwlksnsym  41254  erclwwlksntr  41255  clwlksfclwwlk  41269  eupth0  41382  frgrncvvdeqlem3  41471  av-numclwlk1lem2fo  41525  av-numclwlk2lem2f  41533  av-numclwwlk5lem  41541  lindsrng01  42051
  Copyright terms: Public domain W3C validator