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

Theorem mpcom 38
Description: Modus ponens inference with commutation of antecedents. Commuted form of mpd 15. (Contributed by NM, 17-Mar-1996.)
Hypotheses
Ref Expression
mpcom.1 (𝜓𝜑)
mpcom.2 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
mpcom (𝜓𝜒)

Proof of Theorem mpcom
StepHypRef Expression
1 mpcom.1 . 2 (𝜓𝜑)
2 mpcom.2 . . 3 (𝜑 → (𝜓𝜒))
32com12 32 . 2 (𝜓 → (𝜑𝜒))
41, 3mpd 15 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:  anabsi5  665  axc16i  2453  mo4  2646  sbcn1  3823  sbcim1  3824  sbcbi1  3829  sbcel21v  3841  elimasni  5950  sotri  5981  unixpid  6129  f0rn0  6558  f1ocnv  6621  funbrfv  6710  elfvmptrab1w  6787  f1dom3el3dif  7018  oprabidw  7176  oprabid  7177  oprabv  7203  ndmovordi  7328  elovmporab  7380  elovmporab1w  7381  elovmporab1  7382  elovmpt3rab1  7394  limomss  7573  unielxp  7718  bropfvvvvlem  7777  f1o2ndf1  7809  smogt  7995  tfrlem1  8003  oawordeulem  8170  omass  8196  ecopovtrn  8390  mapfvd  8433  php  8690  unxpdom  8714  findcard2d  8749  findcard3  8750  isfinite2  8765  fsuppimp  8828  fsuppunfi  8842  fsuppunbi  8843  fsuppres  8847  infsupprpr  8957  cantnfval2  9121  cantnfle  9123  cantnfp1lem3  9132  cantnflem1  9141  cnfcom  9152  rankr1ai  9216  rankonidlem  9246  rankxplim2  9298  oncard  9378  ficardom  9379  cardne  9383  acnnum  9467  alephord2i  9492  cardaleph  9504  aceq3lem  9535  dfac5lem5  9542  dfac12lem3  9560  ackbij1lem16  9646  cfslb  9677  cfslb2n  9679  cfsmolem  9681  fin4i  9709  infpssr  9719  fin1a2lem6  9816  axdc3lem2  9862  axcclem  9868  ttukeylem6  9925  fodomb  9937  gchi  10035  fpwwe2lem5  10045  pwfseqlem4  10073  pwfseq  10075  inawina  10101  wunfi  10132  inar1  10186  ltexnq  10386  ltbtwnnq  10389  ltexprlem4  10450  ltexpri  10454  prlem936  10458  suplem1pr  10463  suplem2pr  10464  recexsrlem  10514  mulgt0sr  10516  map2psrpr  10521  supsr  10523  eqlei  10739  eqlei2  10740  ledivp1i  11554  nnind  11645  nnmulcl  11650  nn0ge2m1nn  11953  nnnegz  11973  ublbneg  12322  xmulasslem  12668  ixxssixx  12742  iccshftri  12863  iccshftli  12865  iccdili  12867  icccntri  12869  elfz1b  12966  fzo1fzo0n0  13078  elfzonlteqm1  13103  elfzo0l  13117  ssfzo12  13120  elfzo1elm1fzo0  13128  elfzr  13140  elfzlmr  13141  zmodidfzoimp  13259  mptnn0fsuppr  13357  seqp1  13374  seqcl2  13378  seqfveq2  13382  seqshft2  13386  monoord  13390  seqsplit  13393  seqcaopr3  13395  seqf1olem2a  13398  seqf1o  13401  seqid2  13406  seqhomo  13407  hashf1rn  13703  hashinfxadd  13736  hashf1lem2  13804  seqcoll  13812  hash2pr  13817  pr2pwpr  13827  hashge2el2difr  13829  hash3tr  13838  fi1uzind  13845  brfi1indALT  13848  elovmptnn0wrd  13901  swrdswrd  14057  pfxccatin12lem2a  14079  swrdccat  14087  swrdccatin1d  14095  swrdccatin2d  14096  repswccat  14138  cshwidxmod  14155  relexpsucnnr  14374  rtrclreclem3  14409  rtrclreclem4  14410  dfrtrcl2  14411  relexpindlem  14412  relexpind  14413  rtrclind  14414  cjre  14488  climeu  14902  climub  15008  fsum2d  15116  fsumabs  15146  fsumrlim  15156  fsumo1  15157  fsumiun  15166  prodfn0  15240  prodfrec  15241  ntrivcvg  15243  fprodabs  15318  fprod2d  15325  fprodefsum  15438  ruclem9  15581  dvdsmod0  15603  p1modz1  15604  dvdsmodexp  15605  dvdsabseq  15653  mod2eq1n2dvds  15686  mulsucdiv2z  15692  nno  15723  nn0o  15724  sadcadd  15797  sadadd2  15799  saddisjlem  15803  smuval2  15821  smupval  15827  smueqlem  15829  smumullem  15831  dfgcd2  15884  lcmgcdlem  15940  lcmftp  15970  exprmfct  16038  eulerthlem2  16109  dvdsprmpweqnn  16211  dvdsprmpweqle  16212  pcmpt  16218  vdwlem10  16316  cshwsidrepsw  16417  cshwshashlem1  16419  prmlem1a  16430  setsn0fun  16510  ressval3d  16551  mreexexd  16909  letsr  17827  insubm  17973  ghmghmrn  18317  pmtrfrn  18517  pmtr3ncom  18534  gsmtrcl  18575  psgnsn  18579  sylow1lem1  18654  efginvrel2  18784  efgsrel  18791  cntzcmnss  18892  gsum2dlem2  19022  telgsumfzs  19040  dprdval  19056  ablfac1eulem  19125  pgpfac1  19133  pgpfac  19137  srgpcomp  19213  ring1ne0  19272  rimf1o  19417  rimrhm  19418  brric2  19431  0ringnnzr  19972  mplcoe1  20176  mplcoe3  20177  mplcoe5lem  20178  mplcoe5  20179  mpfaddcl  20248  mpfmulcl  20249  coe1ae0  20314  coe1fzgsumd  20400  gsummoncoe1  20402  pf1addcl  20446  pf1mulcl  20447  evl1gsumd  20450  zrhpsgnelbas  20668  psgndiflemA  20675  mamufacex  20930  mat0dimcrng  21009  mavmulsolcl  21090  mdetunilem9  21159  cramerlem3  21228  pmatcollpw3fi1  21326  pm2mpfo  21352  chmaidscmat  21386  chfacfscmul0  21396  chfacfpmmul0  21400  cpmadugsumlemF  21414  tg2  21503  neindisj2  21661  neiptopnei  21670  t1t0  21886  fiuncmp  21942  hmeof1o  22302  ist1-5lem  22358  t1r0  22359  alexsublem  22582  imasdsf1olem  22912  tgioo  23333  fsumcn  23407  voliunlem3  24082  itgfsum  24356  dvbsss  24429  dvmptfsum  24501  dvfsumlem2  24553  dvfsumlem4  24555  plyco  24760  dgrcolem1  24792  dgrco  24794  dvntaylp  24888  taylthlem1  24890  jensen  25494  bposlem5  25792  lgsqrmodndvds  25857  gausslemma2dlem0i  25868  gausslemma2dlem4  25873  lgsquad2lem2  25889  2lgslem3  25908  2lgs  25911  2lgsoddprm  25920  dchrisum0flb  26014  pntpbnd1  26090  pntlemf  26109  brbtwn  26613  brcgr  26614  umgrnloopv  26819  umgrnloop  26821  usgrnloopvALT  26911  usgrnloopALT  26913  usgredg2vlem2  26936  subgrprop  26983  uvtxnbgrvtx  27103  cusgrsize2inds  27163  rgrprop  27270  rusgrprop  27272  wlkprop  27321  wlkvtxeledg  27333  wlkeq  27343  wlkl1loop  27347  wlk1walk  27348  uspgr2wlkeqi  27357  wlkreslem  27379  wlkres  27380  redwlk  27382  lfgrwlknloop  27399  2pthnloop  27440  usgr2trlncl  27469  usgr2pth  27473  clwlkcompim  27489  clwlkcompbp  27491  uspgrn2crct  27514  crctcshwlkn0  27527  wwlknp  27549  wwlkswwlksn  27571  wlkiswwlks2lem4  27578  wlkiswwlks2  27581  wlklnwwlkln2lem  27588  wwlksnext  27599  wwlksnextbi  27600  wwlksnredwwlkn0  27602  wwlksnextwrd  27603  clwlkclwwlklem2a  27704  clwlkclwwlklem2  27706  clwlkclwwlkflem  27710  clwwisshclwws  27721  clwwlknp  27743  clwwlknwwlksn  27744  clwwlkwwlksb  27761  clwwlkext2edg  27763  umgrhashecclwwlk  27785  clwwlknun  27819  1pthond  27851  upgr3v3e3cycl  27887  upgr4cycl4dv4e  27892  eupth2  27946  3vfriswmgr  27985  3cyclfrgrrn1  27992  n4cyclfrgr  27998  frgrnbnb  28000  frgrncvvdeqlem3  28008  frgrncvvdeqlem6  28011  frgrncvvdeqlem7  28012  frgrncvvdeqlem8  28013  frgrwopreglem4a  28017  frgrwopreg  28030  frgrregorufr0  28031  frgr2wwlkeqm  28038  2clwwlk2clwwlklem  28053  wlkl0  28074  frgrreggt1  28100  frgrregord013  28102  frgrregord13  28103  frgrogt3nreg  28104  friendshipgt3  28105  friendship  28106  blocn2  28513  cvexchlem  30073  cdj3lem2b  30142  cnvoprabOLD  30383  nnindf  30462  issgon  31282  sitgclg  31500  sseqp1  31553  bnj938  32109  bnj964  32115  bnj1052  32145  bnj1125  32162  subfacp1lem6  32330  cvmliftlem7  32436  cvmliftlem10  32439  mclsrcl  32706  pprodss4v  33243  segleantisym  33474  rankeq1o  33530  bj-restv  34281  iooelexlt  34526  relowlssretop  34527  rdgeqoa  34534  matunitlindflem1  34770  poimirlem22  34796  poimirlem25  34799  poimirlem28  34802  poimirlem31  34805  mblfinlem3  34813  mbfresfi  34820  mettrifi  34915  opidon2OLD  35015  isexid2  35016  grpomndo  35036  elghomlem2OLD  35047  rngoidmlem  35097  rngoueqz  35101  iscringd  35159  cdlemk35s  37955  cdlemk39s  37957  cdlemk42  37959  mzpadd  39215  mzpmul  39216  mzpcompact2  39229  dford3lem2  39504  aomclem6  39539  cnsrexpcl  39645  ensucne0OLD  39776  pr2cv  39787  relexpss1d  39930  iunrelexpmin1  39933  iunrelexpmin2  39937  tfindsd  40444  nzin  40530  axc11next  40618  iotavalsb  40645  ssdec  41234  fperiodmullem  41450  monoordxrv  41638  fmul01  41741  fmulcl  41742  fmuldfeqlem1  41743  fmuldfeq  41744  fprodcnlem  41760  iblspltprt  42138  itgspltprt  42144  stoweidlem2  42168  stoweidlem3  42169  stoweidlem6  42172  stoweidlem8  42174  stoweidlem17  42183  stoweidlem19  42185  stoweidlem21  42187  stoweidlem26  42192  stoweidlem31  42197  stoweidlem43  42209  fourierdlem42  42315  funressnfv  43159  eu2ndop1stv  43205  afv0fv0  43229  afv0nbfvbi  43231  funressnbrafv2  43324  funbrafv2  43327  nelbrim  43355  ssfz12  43395  fzoopth  43408  smonoord  43412  iccpartiltu  43429  iccpartigtl  43430  iccelpart  43440  icceuelpart  43443  fargshiftf  43447  fargshiftf1  43448  fargshiftfo  43449  sprel  43493  sprsymrelf1lem  43500  sprsymrelfolem2  43502  prproropf1olem4  43515  lighneallem4  43622  mogoldbblem  43732  fpprnn  43742  fpprwppr  43751  fpprwpprb  43752  sbgoldbwt  43789  bgoldbtbndlem2  43818  bgoldbtbndlem4  43820  tgoldbach  43829  upwlkwlk  43861  clcllaw  43996  intop  44008  clintop  44013  assintop  44014  assintopcllaw  44017  lmod0rng  44037  ringrng  44048  rngimf1o  44074  rngimrnghm  44075  ztprmneprm  44293  scmsuppss  44318  ply1mulgsumlem1  44338  ply1mulgsumlem2  44339  lcoel0  44381  ellcoellss  44388  lindslinindsimp2lem5  44415  ldepspr  44426  flnn0div2ge  44491  nnolog2flm1  44548  blengt1fldiv2p1  44551  dignn0flhalf  44576
  Copyright terms: Public domain W3C validator