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

Step	Hyp	Ref	Expression
1		mpcom.1	. 2 ⊢ (𝜓 → 𝜑)
2		mpcom.2	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
3	2	com12 32	. 2 ⊢ (𝜓 → (𝜑 → 𝜒))
4	1, 3	mpd 15	1 ⊢ (𝜓 → 𝜒)

Syntax hints:   → wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is referenced by:  syldan  583  axc16i  2373  sbcn1  3723  sbcim1  3724  sbcbi1  3728  sbcel21v  3740  elimasni  5794  sotri  5825  unixpid  5971  f0rn0  6391  f1ocnv  6454  funbrfv  6544  f1dom3el3dif  6851  oprabid  7006  oprabv  7032  ndmovordi  7154  elovmporab  7209  elovmporab1  7210  elovmpt3rab1  7222  limomss  7400  unielxp  7538  bropfvvvvlem  7593  f1o2ndf1  7622  smogt  7807  tfrlem1  7815  oawordeulem  7980  omass  8006  ecopovtrn  8199  mapfvd  8242  php  8496  unxpdom  8519  findcard2d  8554  findcard3  8555  isfinite2  8570  fsuppimp  8633  fsuppunfi  8647  fsuppunbi  8648  fsuppres  8652  infsupprpr  8762  cantnfval2  8925  cantnfle  8927  cantnfp1lem3  8936  cantnflem1  8945  cnfcom  8956  rankr1ai  9020  rankonidlem  9050  rankxplim2  9102  oncard  9182  ficardom  9183  cardne  9187  acnnum  9271  alephord2i  9296  cardaleph  9308  aceq3lem  9339  dfac5lem5  9346  dfac12lem3  9364  ackbij1lem16  9454  cfslb  9485  cfslb2n  9487  cfsmolem  9489  fin4i  9517  infpssr  9527  fin1a2lem6  9624  axdc3lem2  9670  axcclem  9676  ttukeylem6  9733  fodomb  9745  gchi  9843  fpwwe2lem5  9853  pwfseqlem4  9881  pwfseq  9883  inawina  9909  wunfi  9940  inar1  9994  ltexnq  10194  ltbtwnnq  10197  ltexprlem4  10258  ltexpri  10262  prlem936  10266  suplem1pr  10271  suplem2pr  10272  recexsrlem  10322  mulgt0sr  10324  map2psrpr  10329  supsr  10331  eqlei  10549  eqlei2  10550  ledivp1i  11365  nnind  11458  nnmulcl  11463  nn0ge2m1nn  11775  nnnegz  11795  ublbneg  12146  xmulasslem  12493  ixxssixx  12567  iccshftri  12688  iccshftli  12690  iccdili  12692  icccntri  12694  elfz1b  12791  fzo1fzo0n0  12902  elfzonlteqm1  12927  elfzo0l  12941  ssfzo12  12944  elfzo1elm1fzo0  12952  elfzr  12964  elfzlmr  12965  zmodidfzoimp  13083  mptnn0fsuppr  13181  seqp1  13198  seqcl2  13202  seqfveq2  13206  seqshft2  13210  monoord  13214  seqsplit  13217  seqcaopr3  13219  seqf1olem2a  13222  seqf1o  13225  seqid2  13230  seqhomo  13231  hashf1rn  13527  hashinfxadd  13558  hashf1lem2  13626  seqcoll  13634  hash2pr  13637  pr2pwpr  13647  hashge2el2difr  13649  hash3tr  13658  fi1uzind  13665  brfi1indALT  13668  elovmptnn0wrd  13721  swrdswrd  13886  swrdccatin12lem2a  13925  swrdccat  13937  swrdccatOLD  13938  swrdccatin1d  13950  swrdccatin2d  13951  swrdccatin12dOLD  13953  repswccat  14004  cshwidxmod  14026  relexpsucnnr  14244  rtrclreclem3  14279  rtrclreclem4  14280  dfrtrcl2  14281  relexpindlem  14282  relexpind  14283  rtrclind  14284  cjre  14358  climeu  14772  climub  14878  fsum2d  14985  fsumabs  15015  fsumrlim  15025  fsumo1  15026  fsumiun  15035  prodfn0  15109  prodfrec  15110  ntrivcvg  15112  fprodabs  15187  fprod2d  15194  fprodefsum  15307  ruclem9  15450  dvdsmod0  15472  p1modz1  15473  dvdsmodexp  15474  dvdsabseq  15522  mod2eq1n2dvds  15555  mulsucdiv2z  15561  nno  15592  nn0o  15593  sadcadd  15666  sadadd2  15668  saddisjlem  15672  smuval2  15690  smupval  15696  smueqlem  15698  smumullem  15700  dfgcd2  15749  lcmgcdlem  15805  lcmftp  15835  exprmfct  15903  eulerthlem2  15974  dvdsprmpweqnn  16076  dvdsprmpweqle  16077  pcmpt  16083  vdwlem10  16181  cshwsidrepsw  16282  cshwshashlem1  16284  prmlem1a  16295  setsn0fun  16375  ressval3d  16416  mreexexd  16790  letsr  17708  ghmghmrn  18161  pmtrfrn  18360  pmtr3ncom  18377  gsmtrcl  18419  psgnsn  18423  sylow1lem1  18497  efginvrel2  18624  efgsrel  18631  cntzcmnss  18732  gsum2dlem2  18857  telgsumfzs  18872  dprdval  18888  ablfac1eulem  18957  pgpfac1  18965  pgpfac  18969  srgpcomp  19018  ring1ne0  19077  rimf1o  19222  rimrhm  19223  brric2  19236  0ringnnzr  19776  mplcoe1  19972  mplcoe3  19973  mplcoe5lem  19974  mplcoe5  19975  mpfaddcl  20040  mpfmulcl  20041  coe1ae0  20103  coe1fzgsumd  20189  gsummoncoe1  20191  pf1addcl  20234  pf1mulcl  20235  evl1gsumd  20238  zrhpsgnelbas  20456  psgndiflemA  20463  mamufacex  20718  mat0dimcrng  20799  mavmulsolcl  20880  mdetunilem9  20949  cramerlem3  21018  pmatcollpw3fi1  21116  pm2mpfo  21142  chmaidscmat  21176  chfacfscmul0  21186  chfacfpmmul0  21190  cpmadugsumlemF  21204  tg2  21293  neindisj2  21451  neiptopnei  21460  t1t0  21676  fiuncmp  21732  hmeof1o  22092  ist1-5lem  22148  t1r0  22149  alexsublem  22372  imasdsf1olem  22702  tgioo  23123  fsumcn  23197  voliunlem3  23872  itgfsum  24146  dvbsss  24219  dvmptfsum  24291  dvfsumlem2  24343  dvfsumlem4  24345  plyco  24550  dgrcolem1  24582  dgrco  24584  dvntaylp  24678  taylthlem1  24680  jensen  25284  bposlem5  25582  lgsqrmodndvds  25647  gausslemma2dlem0i  25658  gausslemma2dlem4  25663  lgsquad2lem2  25679  2lgslem3  25698  2lgs  25701  2lgsoddprm  25710  dchrisum0flb  25804  pntpbnd1  25880  pntlemf  25899  brbtwn  26404  brcgr  26405  umgrnloopv  26610  umgrnloop  26612  usgrnloopvALT  26702  usgrnloopALT  26704  usgredg2vlem2  26727  subgrprop  26774  uvtxnbgrvtx  26894  cusgrsize2inds  26954  rgrprop  27061  rusgrprop  27063  wlkprop  27112  wlkvtxeledg  27124  wlkeq  27134  wlkl1loop  27138  wlk1walk  27139  uspgr2wlkeqi  27148  wlkreslem  27171  wlkres  27172  wlkreslemOLD  27173  wlkresOLD  27174  redwlk  27176  lfgrwlknloop  27193  2pthnloop  27236  usgr2trlncl  27265  usgr2pth  27269  clwlkcompim  27285  clwlkcompbp  27287  uspgrn2crct  27310  crctcshwlkn0  27323  wwlknp  27345  wwlkswwlksn  27367  wlkiswwlks2lem4  27374  wlkiswwlks2  27377  wlklnwwlkln2lem  27385  wwlksnext  27397  wwlksnextbi  27398  wwlksnextbiOLD  27399  wwlksnredwwlkn0  27402  wwlksnredwwlkn0OLD  27403  wwlksnextwrd  27404  wwlksnextwrdOLD  27409  clwlkclwwlklem2a  27520  clwlkclwwlklem2  27522  clwlkclwwlkflem  27528  clwwisshclwws  27546  clwwlknp  27568  clwwlknwwlksn  27569  clwwlkwwlksb  27593  clwwlkext2edg  27595  umgrhashecclwwlk  27618  clwwlknun  27656  1pthond  27689  upgr3v3e3cycl  27725  upgr4cycl4dv4e  27730  eupth2  27785  3vfriswmgr  27828  3cyclfrgrrn1  27835  n4cyclfrgr  27841  frgrnbnb  27843  frgrncvvdeqlem3  27851  frgrncvvdeqlem6  27854  frgrncvvdeqlem7  27855  frgrncvvdeqlem8  27856  frgrwopreglem4a  27860  frgrwopreg  27873  frgrregorufr0  27874  frgr2wwlkeqm  27881  2clwwlk2clwwlklem  27899  wlkl0  27936  frgrreggt1  27966  frgrregord013  27968  frgrregord13  27969  frgrogt3nreg  27970  friendshipgt3  27971  friendship  27972  blocn2  28378  cvexchlem  29942  cdj3lem2b  30011  cnvoprabOLD  30233  nnindf  30306  issgon  31060  sitgclg  31278  sseqp1  31332  bnj938  31889  bnj964  31895  bnj1052  31925  bnj1125  31942  subfacp1lem6  32050  cvmliftlem7  32156  cvmliftlem10  32159  mclsrcl  32361  pprodss4v  32899  segleantisym  33130  rankeq1o  33186  bj-elep  33902  bj-restv  33929  iooelexlt  34118  relowlssretop  34119  rdgeqoa  34126  matunitlindflem1  34362  poimirlem22  34388  poimirlem25  34391  poimirlem28  34394  poimirlem31  34397  mblfinlem3  34405  mbfresfi  34412  mettrifi  34507  opidon2OLD  34607  isexid2  34608  grpomndo  34628  elghomlem2OLD  34639  rngoidmlem  34689  rngoueqz  34693  iscringd  34751  cdlemk35s  37551  cdlemk39s  37553  cdlemk42  37555  mzpadd  38764  mzpmul  38765  mzpcompact2  38778  dford3lem2  39054  aomclem6  39089  cnsrexpcl  39195  relexpss1d  39447  iunrelexpmin1  39450  iunrelexpmin2  39454  tfindsd  39973  nzin  40100  axc11next  40189  iotavalsb  40216  ssdec  40807  fperiodmullem  41029  monoordxrv  41219  fmul01  41322  fmulcl  41323  fmuldfeqlem1  41324  fmuldfeq  41325  fprodcnlem  41341  iblspltprt  41718  itgspltprt  41724  stoweidlem2  41748  stoweidlem3  41749  stoweidlem6  41752  stoweidlem8  41754  stoweidlem17  41763  stoweidlem19  41765  stoweidlem21  41767  stoweidlem26  41772  stoweidlem31  41777  stoweidlem43  41789  fourierdlem42  41895  funressnfv  42713  eu2ndop1stv  42760  afv0fv0  42784  afv0nbfvbi  42786  funressnbrafv2  42879  funbrafv2  42882  nelbrim  42910  ssfz12  42950  fzoopth  42963  smonoord  42967  iccpartiltu  42984  iccpartigtl  42985  iccelpart  42995  icceuelpart  42998  fargshiftf  43002  fargshiftf1  43003  fargshiftfo  43004  sprel  43044  sprsymrelf1lem  43051  sprsymrelfolem2  43053  prproropf1olem4  43066  lighneallem4  43173  mogoldbblem  43283  fpprnn  43293  fpprwppr  43302  fpprwpprb  43303  sbgoldbwt  43340  bgoldbtbndlem2  43369  bgoldbtbndlem4  43371  tgoldbach  43380  upwlkwlk  43412  clcllaw  43492  intop  43504  clintop  43509  assintop  43510  assintopcllaw  43513  lmod0rng  43533  ringrng  43544  rngimf1o  43570  rngimrnghm  43571  ztprmneprm  43789  scmsuppss  43816  ply1mulgsumlem1  43837  ply1mulgsumlem2  43838  lcoel0  43880  ellcoellss  43887  lindslinindsimp2lem5  43914  ldepspr  43925  flnn0div2ge  43991  nnolog2flm1  44048  blengt1fldiv2p1  44051  dignn0flhalf  44076