Theorem mpcom 39

Description: Modus ponens inference with commutation of antecedents. Commuted form of mpd 16. (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 33	. 2 ⊢ (𝜓 → (𝜑 → 𝜒))
4	1, 3	mpd 16	1 ⊢ (𝜓 → 𝜒)

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  anabsi5  682  axc16i  2471  mo4  2597  sbcn1  3799  sbcim1  3800  sbcbi1  3804  sbcel21v  3814  sbccomlem  3825  csbie2df  4411  elimasni  6098  sotri  6132  unixpid  6292  f0rn0  6770  f1ocnv  6840  funbrfv  6936  elfvmptrab1w  7024  f1dom3el3dif  7274  oprabidw  7454  oprabid  7455  oprabv  7483  ndmovordi  7614  elovmporab  7669  elovmporab1w  7670  elovmporab1  7671  elovmpt3rab1  7683  limomss  7876  unielxp  8033  bropfvvvvlem  8095  f1o2ndf1  8126  smogt  8363  tfrlem1  8371  oawordeulem  8548  omass  8574  ecopovtrn  8827  mapfvd  8886  findcard2d  9161  ssfi  9167  f1domfi  9175  php  9201  unxpdom  9229  findcard3  9253  isfinite2  9268  fsuppimp  9338  fsuppunfi  9358  fsuppunbi  9359  fsuppres  9363  infsupprpr  9476  cantnfval2  9648  cantnfle  9650  cantnfp1lem3  9659  cantnflem1  9668  cnfcom  9679  rankr1ai  9780  rankonidlem  9810  rankxplim2  9862  oncard  9965  ficardom  9966  cardne  9970  acnnum  10055  alephord2i  10080  cardaleph  10092  aceq3lem  10123  dfac5lem5  10130  dfac12lem3  10148  ackbij1lem16  10236  cfslb  10268  cfslb2n  10270  cfsmolem  10272  fin4i  10300  infpssr  10310  fin1a2lem6  10407  axdc3lem2  10453  axcclem  10459  ttukeylem6  10516  fodomb  10528  gchi  10627  pwfseq  10667  inawina  10693  wunfi  10724  inar1  10778  ltexnq  10978  ltbtwnnq  10981  ltexprlem4  11042  ltexpri  11046  prlem936  11050  suplem1pr  11055  suplem2pr  11056  recexsrlem  11106  mulgt0sr  11108  map2psrpr  11113  supsr  11115  eqlei  11338  eqlei2  11339  ledivp1i  12158  nnind  12269  nnmulcl  12275  nn0ge2m1nn  12592  nnnegz  12612  ublbneg  12975  xmulasslem  13329  ixxssixx  13404  iccshftri  13532  iccshftli  13534  iccdili  13536  icccntri  13538  elfz1b  13640  fzo1fzo0n0  13763  elfzonlteqm1  13789  elfzo0l  13804  ssfzo12  13807  fzoopth  13810  elfzo1elm1fzo0  13816  elfzr  13829  elfzlmr  13830  zmodidfzoimp  13954  mptnn0fsuppr  14055  seqp1  14072  seqcl2  14076  seqfveq2  14080  seqshft2  14084  monoord  14088  seqsplit  14091  seqcaopr3  14093  seqf1olem2a  14096  seqf1o  14099  seqid2  14104  seqhomo  14105  hashf1rn  14408  hashinfxadd  14441  hashf1lem2  14513  seqcoll  14521  hash2pr  14526  pr2pwpr  14536  hashge2el2difr  14538  hash3tr  14548  fi1uzind  14564  brfi1indALT  14567  elovmptnn0wrd  14616  swrdswrd  14766  pfxccatin12lem2a  14788  swrdccat  14796  swrdccatin1d  14804  swrdccatin2d  14805  repswccat  14849  cshwidxmod  14866  relexpsucnnr  15088  rtrclreclem3  15123  rtrclreclem4  15124  dfrtrcl2  15125  relexpindlem  15126  relexpind  15127  rtrclind  15128  cjre  15216  climeu  15632  climub  15739  fsum2d  15848  fsumabs  15879  fsumrlim  15889  fsumo1  15890  fsumiun  15899  prodfn0  15974  prodfrec  15975  ntrivcvg  15977  fprodabs  16054  fprod2d  16061  fprodefsum  16174  ruclem9  16319  dvdsmod0  16341  p1modz1  16342  dvdsmodexp  16343  dvdsabseq  16396  mod2eq1n2dvds  16430  mulsucdiv2z  16436  nno  16465  nn0o  16466  sadcadd  16541  sadadd2  16543  saddisjlem  16547  smuval2  16565  smupval  16571  smueqlem  16573  smumullem  16575  dfgcd2  16629  lcmgcdlem  16689  lcmftp  16719  exprmfct  16788  eulerthlem2  16866  dvdsprmpweqnn  16970  dvdsprmpweqle  16971  pcmpt  16977  vdwlem10  17075  cshwsidrepsw  17178  cshwshashlem1  17180  prmlem1a  17191  setsn0fun  17258  ressval3d  17331  mreexexd  17729  letsr  18674  insubm  18908  ghmghmrn  19336  pmtrfrn  19559  pmtr3ncom  19576  gsmtrcl  19617  psgnsn  19621  sylow1lem1  19699  efginvrel2  19828  efgsrel  19835  cntzcmnss  19942  gsum2dlem2  20072  telgsumfzs  20090  dprdval  20106  ablfac1eulem  20175  pgpfac1  20183  pgpfac  20187  srgpcomp  20331  ringrng  20400  ring1ne0  20415  rngimf1o  20569  rngimrnghm  20570  rngimcnv  20571  0ringnnzr  20660  zrhpsgnelbas  21781  psgndiflemA  21788  mplcoe1  22225  mplcoe3  22226  mplcoe5lem  22227  mplcoe5  22228  mpfaddcl  22301  mpfmulcl  22302  coe1ae0  22413  coe1fzgsumd  22501  gsummoncoe1  22505  pf1addcl  22550  pf1mulcl  22551  evl1gsumd  22554  mamufacex  22590  mat0dimcrng  22664  mavmulsolcl  22745  mdetunilem9  22814  cramerlem3  22883  pmatcollpw3fi1  22982  pm2mpfo  23008  chmaidscmat  23042  chfacfscmul0  23052  chfacfpmmul0  23056  cpmadugsumlemF  23070  tg2  23159  neindisj2  23317  neiptopnei  23326  t1t0  23542  fiuncmp  23598  hmeof1o  23958  ist1-5lem  24014  t1r0  24015  alexsublem  24238  imasdsf1olem  24567  tgioo  24990  fsumcn  25066  voliunlem3  25748  itgfsum  26023  dvbsss  26098  dvmptfsum  26171  dvfsumlem2  26223  dvfsumlem4  26225  plyco  26435  dgrcolem1  26467  dgrco  26469  dvntaylp  26571  taylthlem1  26573  jensen  27190  bposlem5  27489  lgsqrmodndvds  27554  gausslemma2dlem0i  27565  gausslemma2dlem4  27570  lgsquad2lem2  27586  2lgslem3  27605  2lgs  27608  2lgsoddprm  27617  dchrisum0flb  27711  pntpbnd1  27787  pntlemf  27806  madebdayim  28118  oldbdayim  28119  pw2cut  28690  brbtwn  29286  brcgr  29287  umgrnloopv  29493  umgrnloop  29495  usgrnloopvALT  29588  usgrnloopALT  29590  usgredg2vlem2  29613  subgrprop  29660  uvtxnbgrvtx  29780  cusgrsize2inds  29840  rgrprop  29947  rusgrprop  29949  wlkprop  29998  wlkvtxeledg  30010  wlkeq  30020  wlkl1loop  30024  wlk1walk  30025  uspgr2wlkeqi  30034  wlkreslem  30054  wlkres  30055  redwlk  30057  lfgrwlknloop  30074  2pthnloop  30117  usgr2trlncl  30146  usgr2pth  30150  clwlkcompim  30166  clwlkcompbp  30168  uspgrn2crct  30194  crctcshwlkn0  30207  wwlknp  30229  wwlkswwlksn  30251  wlkiswwlks2lem4  30258  wlkiswwlks2  30261  wlklnwwlkln2lem  30268  wwlksnext  30279  wwlksnextbi  30280  wwlksnredwwlkn0  30282  wwlksnextwrd  30283  clwlkclwwlklem2a  30386  clwlkclwwlklem2  30388  clwlkclwwlkflem  30392  clwwisshclwws  30403  clwwlknp  30425  clwwlknwwlksn  30426  clwwlkwwlksb  30442  clwwlkext2edg  30444  umgrhashecclwwlk  30466  clwwlknun  30500  1pthond  30532  upgr3v3e3cycl  30568  upgr4cycl4dv4e  30573  eupth2  30627  3vfriswmgr  30666  3cyclfrgrrn1  30673  n4cyclfrgr  30679  frgrnbnb  30681  frgrncvvdeqlem3  30689  frgrncvvdeqlem6  30692  frgrncvvdeqlem7  30693  frgrncvvdeqlem8  30694  frgrwopreglem4a  30698  frgrwopreg  30711  frgrregorufr0  30712  frgr2wwlkeqm  30719  2clwwlk2clwwlklem  30734  wlkl0  30755  frgrreggt1  30781  frgrregord013  30783  frgrregord13  30784  frgrogt3nreg  30785  friendshipgt3  30786  friendship  30787  blocn2  31197  cvexchlem  32757  cdj3lem2b  32826  nnindf  33201  gsumwun  33427  domnprodn0  33629  issgon  34544  sitgclg  34763  sseqp1  34816  bnj938  35356  bnj964  35362  bnj1052  35394  bnj1125  35411  onvf1odlem4  35613  subfacp1lem6  35697  cvmliftlem7  35803  cvmliftlem10  35806  mclsrcl  36073  pprodss4v  36394  segleantisym  36627  rankeq1o  36683  bj-restv  37777  iooelexlt  38048  relowlssretop  38049  rdgeqoa  38056  matunitlindflem1  38307  poimirlem22  38333  poimirlem25  38336  poimirlem28  38339  poimirlem31  38342  mblfinlem3  38350  mbfresfi  38357  mettrifi  38448  opidon2OLD  38545  isexid2  38546  grpomndo  38566  elghomlem2OLD  38577  rngoidmlem  38627  rngoueqz  38631  iscringd  38689  cdlemk35s  41751  cdlemk39s  41753  cdlemk42  41755  uzindd  42785  mzpadd  43509  mzpmul  43510  mzpcompact2  43523  dford3lem2  43794  aomclem6  43826  cnsrexpcl  43932  ensucne0OLD  44296  pr2cv  44314  relexpss1d  44471  iunrelexpmin1  44474  iunrelexpmin2  44478  tfindsd  44974  nzin  45068  axc11next  45156  iotavalsb  45183  ssdec  45846  fperiodmullem  46062  monoordxrv  46235  fmul01  46336  fmulcl  46337  fmuldfeqlem1  46338  fmuldfeq  46339  iblspltprt  46727  itgspltprt  46733  stoweidlem2  46756  stoweidlem3  46757  stoweidlem6  46760  stoweidlem8  46762  stoweidlem17  46771  stoweidlem19  46773  stoweidlem21  46775  stoweidlem26  46780  stoweidlem31  46785  stoweidlem43  46797  fourierdlem42  46903  funressnfv  47820  eu2ndop1stv  47902  afv0fv0  47926  afv0nbfvbi  47928  funressnbrafv2  48021  funbrafv2  48024  nelbrim  48052  ssfz12  48091  smonoord  48154  iccpartiltu  48211  iccpartigtl  48212  iccelpart  48222  icceuelpart  48225  fargshiftf  48229  fargshiftf1  48230  fargshiftfo  48231  sprel  48273  sprsymrelf1lem  48280  sprsymrelfolem2  48282  prproropf1olem4  48295  lighneallem4  48402  mogoldbblem  48525  fpprnn  48535  fpprwppr  48544  fpprwpprb  48545  sbgoldbwt  48582  bgoldbtbndlem2  48611  bgoldbtbndlem4  48613  tgoldbach  48622  grimprop  48688  grlimprop  48789  grilcbri2  48816  upwlkwlk  48944  clcllaw  48996  intop  49008  clintop  49013  assintop  49014  assintopcllaw  49017  lmod0rng  49034  ztprmneprm  49167  scmsuppss  49191  ply1mulgsumlem1  49206  ply1mulgsumlem2  49207  lcoel0  49248  ellcoellss  49255  lindslinindsimp2lem5  49282  ldepspr  49293  flnn0div2ge  49353  nnolog2flm1  49410  blengt1fldiv2p1  49413  dignn0flhalf  49438  naryfvalelfv  49452  0aryfvalelfv  49455  fv1arycl  49457  fv2arycl  49468