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

Theorem mpancom 684
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 584 1 (𝜓𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396
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 208  df-an 397
This theorem is referenced by:  mpan  686  spesbc  3868  xpiindi  5704  fununfun  6398  dffv2  6752  fliftcnv  7059  riotaprop  7136  elovmpt3rab1  7398  3xpexg  7467  orduniorsuc  7536  unielxp  7721  dmtpos  7898  tpossym  7918  wfrlem5  7953  oesuclem  8144  ercnv  8303  cnvct  8578  undom  8597  sucxpdom  8719  3xpfi  8782  pwfilem  8810  rankr1id  9283  cardnn  9384  alephnbtwn2  9490  alephsucdom  9497  cdainflem  9605  isfin4p1  9729  axcclem  9871  dmct  9938  mptct  9952  infxpidm  9976  fpwwe2lem9  10052  gchpwdom  10084  elwina  10100  elina  10101  rankcf  10191  ltexprlem4  10453  lem1  11475  ltdivp1i  11558  rpnnen1lem5  12373  eluzfz1  12907  fzpred  12948  uznfz  12983  fz0fzdiffz0  13009  fzctr  13012  flid  13171  modid0  13258  2txmodxeq0  13292  faclbnd3  13645  faclbnd4lem4  13649  bcn1  13666  hashfac  13809  repswsymballbi  14135  wrdlen2i  14297  dfrtrclrec2  14409  rtrclreclem3  14412  rtrclreclem4  14413  relexpindlem  14415  sqrtsq  14622  absrdbnd  14694  sqreulem  14712  sqreu  14713  bpoly2  15404  bpoly3  15405  gcd0id  15860  lcmgcdlem  15943  lcmftp  15973  dvdsnprmd  16027  2mulprm  16030  pcprod  16224  fldivp1  16226  invsym2  17026  pleval2i  17567  smndlsmidm  18704  subrgsubm  19471  cncrng  20485  znchr  20628  mattposvs  20983  smadiadetglem2  21200  tg1  21491  cldval  21550  cldss  21556  cldopn  21558  1stcrestlem  21979  refbas  22037  refssex  22038  regr1  22277  kqreg  22278  kqnrm  22279  ufilen  22457  symgtgp  22628  elrnust  22751  psmetdmdm  22833  metuval  23077  icoopnst  23461  cnheiborlem  23476  cfilfcls  23795  eflogeq  25101  logdivlt  25120  logdifbnd  25488  harmonicbnd4  25505  basellem5  25579  bposlem7  25783  zabsle1  25789  addsqn2reu  25934  chto1ub  25969  chpo1ub  25973  vmadivsum  25975  dchrmusum2  25987  dchrvmasum2if  25990  dchrvmasumlema  25993  dchrvmasumiflem2  25995  dchrisum0re  26006  dchrvmasumlem  26016  rplogsum  26020  mulogsumlem  26024  logdivsum  26026  selberg2lem  26043  pntrmax  26057  pntlem3  26102  pntleml  26104  pnt2  26106  usgredg2vlem2  26925  vtxdgelxnn0  27171  wlkonprop  27357  wksonproplem  27403  wwlknbp  27537  wspthnp  27545  wlklnwwlkln1  27563  clwwlkf  27743  erclwwlknsym  27766  erclwwlkntr  27767  eupth0  27910  numclwwlk1lem2fo  28054  numclwlk2lem2f  28073  numclwwlk5lem  28083  hilablo  28854  hhssabloilem  28955  mayete3i  29422  homulid2  29494  adjeu  29583  lnopeqi  29702  cnlnadjlem7  29767  adjbdlnb  29778  nmopcoadji  29795  bracnlnval  29808  elunirn2  30314  mptctf  30369  xraddge02  30396  xrge0npcan  30598  gsumle  30642  gsumvsca1  30771  gsumvsca2  30772  metidval  31019  pstmval  31024  baselsiga  31263  sigasspw  31264  ddeval1  31382  ddeval0  31383  braew  31390  derangen2  32308  subfaclim  32322  snmlff  32463  elfzm12  32805  noextendlt  33063  fnetr  33586  wl-sbal1  34669  poimirlem13  34775  poimirlem14  34776  poimirlem31  34793  poimirlem32  34794  ismblfin  34803  itg2addnclem2  34814  areacirclem2  34853  areacirc  34857  ismgmOLD  34999  ismndo2  35023  rngomndo  35084  cnvepimaex  35464  dmqseq  35745  prter3  35888  atbase  36295  llnbase  36515  lplnbase  36540  lvolbase  36584  lhpbase  37004  rernegcl  39069  renegadd  39070  reneg0addid2  39072  sn-0ne2  39104  3cubes  39155  mzpsubmpt  39208  mzpnegmpt  39209  eliunov2  39892  iunrelexp0  39915  enmappwid  40214  uunT1  40982  nnfoctb  41177  afveu  43221  afv2eu  43306  afv20fv0  43331  fzopredsuc  43392  fargshiftfva  43438  lindsrng01  44358
  Copyright terms: Public domain W3C validator