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  2465  mo4  2591  sbcn1  3790  sbcim1  3791  sbcbi1  3795  sbcel21v  3805  sbccomlem  3816  csbie2df  4400  elimasni  6088  sotri  6120  unixpid  6287  f0rn0  6767  f1ocnv  6837  funbrfv  6933  elfvmptrab1w  7021  f1dom3el3dif  7273  oprabidw  7451  oprabid  7452  oprabv  7480  ndmovordi  7612  elovmporab  7667  elovmporab1w  7668  elovmporab1  7669  elovmpt3rab1  7681  limomss  7882  unielxp  8039  bropfvvvvlem  8102  f1o2ndf1  8135  smogt  8378  tfrlem1  8386  oawordeulem  8565  omass  8591  ecopovtrn  8844  mapfvd  8910  findcard2d  9185  ssfi  9191  f1domfi  9199  php  9225  unxpdom  9253  findcard3  9277  isfinite2  9293  fsuppimp  9363  fsuppunfi  9383  fsuppunbi  9384  fsuppres  9388  infsupprpr  9501  cantnfval2  9673  cantnfle  9675  cantnfp1lem3  9684  cantnflem1  9693  cnfcom  9704  rankr1ai  9809  rankonidlem  9841  rankxplim2  9900  oncard  10044  ficardom  10045  cardne  10049  acnnum  10134  alephord2i  10159  cardaleph  10171  aceq3lem  10202  dfac5lem5  10209  dfac12lem3  10227  ackbij1lem16  10315  cfslb  10347  cfslb2n  10349  cfsmolem  10351  fin4i  10379  infpssr  10389  fin1a2lem6  10486  axdc3lem2  10532  axcclem  10538  ttukeylem6  10595  fodomb  10608  gchi  10712  pwfseq  10752  inawina  10778  wunfi  10809  inar1  10863  ltexnq  11063  ltbtwnnq  11066  ltexprlem4  11127  ltexpri  11131  prlem936  11135  suplem1pr  11140  suplem2pr  11141  recexsrlem  11191  mulgt0sr  11193  map2psrpr  11198  supsr  11200  eqlei  11423  eqlei2  11424  ledivp1i  12245  nnind  12356  nnmulcl  12362  nn0ge2m1nn  12679  nnnegz  12699  ublbneg  13063  xmulasslem  13418  ixxssixx  13493  iccshftri  13621  iccshftli  13623  iccdili  13625  icccntri  13627  elfz1b  13730  fzo1fzo0n0  13853  elfzonlteqm1  13879  elfzo0l  13894  ssfzo12  13897  fzoopth  13900  elfzo1elm1fzo0  13906  elfzr  13919  elfzlmr  13920  zmodidfzoimp  14044  mptnn0fsuppr  14145  seqp1  14162  seqcl2  14166  seqfveq2  14170  seqshft2  14174  monoord  14178  seqsplit  14181  seqcaopr3  14183  seqf1olem2a  14186  seqf1o  14189  seqid2  14194  seqhomo  14195  hashf1rn  14499  hashinfxadd  14532  hashf1lem2  14604  seqcoll  14612  hash2pr  14617  pr2pwpr  14627  hashge2el2difr  14629  hash3tr  14639  fi1uzind  14655  brfi1indALT  14658  elovmptnn0wrd  14707  swrdswrd  14858  pfxccatin12lem2a  14880  swrdccat  14888  swrdccatin1d  14896  swrdccatin2d  14897  repswccat  14941  cshwidxmod  14958  relexpsucnnr  15183  rtrclreclem3  15218  rtrclreclem4  15219  dfrtrcl2  15220  relexpindlem  15221  relexpind  15222  rtrclind  15223  cjre  15311  climeu  15727  climub  15834  fsum2d  15942  fsumabs  15973  fsumrlim  15983  fsumo1  15984  fsumiun  15993  prodfn0  16068  prodfrec  16069  ntrivcvg  16071  fprodabs  16146  fprod2d  16153  fprodefsum  16266  ruclem9  16411  dvdsmod0  16433  p1modz1  16434  dvdsmodexp  16435  dvdsabseq  16488  mod2eq1n2dvds  16522  mulsucdiv2z  16528  nno  16557  nn0o  16558  sadcadd  16633  sadadd2  16635  saddisjlem  16639  smuval2  16657  smupval  16663  smueqlem  16665  smumullem  16667  dfgcd2  16724  lcmgcdlem  16786  lcmftp  16816  exprmfct  16885  eulerthlem2  16964  dvdsprmpweqnn  17068  dvdsprmpweqle  17069  pcmpt  17075  vdwlem10  17173  cshwsidrepsw  17276  cshwshashlem1  17278  prmlem1a  17289  setsn0fun  17356  ressval3d  17429  mreexexd  17827  letsr  18772  insubm  19019  ghmghmrn  19454  pmtrfrn  19677  pmtr3ncom  19694  gsmtrcl  19735  psgnsn  19739  sylow1lem1  19817  efginvrel2  19946  efgsrel  19953  cntzcmnss  20060  gsum2dlem2  20190  telgsumfzs  20208  dprdval  20224  ablfac1eulem  20293  pgpfac1  20301  pgpfac  20305  srgpcomp  20449  ringrng  20519  ring1ne0  20535  rngimf1o  20689  rngimrnghm  20690  rngimcnv  20691  0ringnnzr  20781  zrhpsgnelbas  21905  psgndiflemA  21912  mplcoe1  22351  mplcoe3  22352  mplcoe5lem  22353  mplcoe5  22354  mpfaddcl  22427  mpfmulcl  22428  coe1ae0  22539  coe1fzgsumd  22627  gsummoncoe1  22631  pf1addcl  22676  pf1mulcl  22677  evl1gsumd  22680  mamufacex  22716  mat0dimcrng  22790  mavmulsolcl  22871  mdetunilem9  22940  matunitlindflem1  22999  cramerlem3  23012  pmatcollpw3fi1  23111  pm2mpfo  23137  chmaidscmat  23171  chfacfscmul0  23181  chfacfpmmul0  23185  cpmadugsumlemF  23199  tg2  23288  neindisj2  23446  neiptopnei  23455  t1t0  23671  fiuncmp  23727  hmeof1o  24088  ist1-5lem  24144  t1r0  24145  alexsublem  24368  imasdsf1olem  24697  tgioo  25120  fsumcn  25196  voliunlem3  25878  itgfsum  26152  dvbsss  26227  dvmptfsum  26300  dvfsumlem2  26352  dvfsumlem4  26354  plyco  26565  dgrcolem1  26597  dgrco  26599  dvntaylp  26703  taylthlem1  26705  jensen  27321  bposlem5  27620  lgsqrmodndvds  27685  gausslemma2dlem0i  27696  gausslemma2dlem4  27701  lgsquad2lem2  27717  2lgslem3  27736  2lgs  27739  2lgsoddprm  27748  dchrisum0flb  27842  pntpbnd1  27918  pntlemf  27937  madebdayim  28279  oldbdayim  28280  pw2cut  28851  brbtwn  29482  brcgr  29483  umgrnloopv  29689  umgrnloop  29691  usgrnloopvALT  29787  usgrnloopALT  29789  usgredg2vlem2  29812  subgrprop  29859  uvtxnbgrvtx  29979  cusgrsize2inds  30039  rgrprop  30146  rusgrprop  30148  wlkprop  30197  wlkvtxeledg  30209  wlkeq  30219  wlkl1loop  30223  wlk1walk  30224  uspgr2wlkeqi  30233  wlkreslem  30253  wlkres  30254  redwlk  30256  lfgrwlknloop  30277  2pthnloop  30322  usgr2trlncl  30351  usgr2pth  30355  clwlkcompim  30372  clwlkcompbp  30374  uspgrn2crct  30402  crctcshwlkn0  30415  wwlknp  30437  wwlkswwlksn  30459  wlkiswwlks2lem4  30466  wlkiswwlks2  30469  wlklnwwlkln2lem  30476  wwlksnext  30487  wwlksnextbi  30488  wwlksnredwwlkn0  30490  wwlksnextwrd  30491  clwlkclwwlklem2a  30594  clwlkclwwlklem2  30596  clwlkclwwlkflem  30600  clwwisshclwws  30611  clwwlknp  30633  clwwlknwwlksn  30634  clwwlkwwlksb  30650  clwwlkext2edg  30652  umgrhashecclwwlk  30674  clwwlknun  30708  1pthond  30740  upgr3v3e3cycl  30786  upgr4cycl4dv4e  30791  eupth2  30845  3vfriswmgr  30884  3cyclfrgrrn1  30891  n4cyclfrgr  30897  frgrnbnb  30899  frgrncvvdeqlem3  30907  frgrncvvdeqlem6  30910  frgrncvvdeqlem7  30911  frgrncvvdeqlem8  30912  frgrwopreglem4a  30916  frgrwopreg  30929  frgrregorufr0  30930  frgr2wwlkeqm  30937  2clwwlk2clwwlklem  30952  wlkl0  30973  frgrreggt1  30999  frgrregord013  31001  frgrregord13  31002  frgrogt3nreg  31003  friendshipgt3  31004  friendship  31005  blocn2  31415  cvexchlem  32975  cdj3lem2b  33044  nnindf  33457  gsumwun  33683  domnprodn0  33885  issgon  34801  sitgclg  35020  sseqp1  35073  bnj938  35613  bnj964  35619  bnj1052  35651  bnj1125  35668  onvf1odlem4  35953  subfacp1lem6  36036  cvmliftlem7  36142  cvmliftlem10  36145  mclsrcl  36412  pprodss4v  36738  segleantisym  36972  rankeq1o  37024  bj-restv  38108  iooelexlt  38378  relowlssretop  38379  rdgeqoa  38386  poimirlem22  38653  poimirlem25  38656  poimirlem28  38659  poimirlem31  38662  mblfinlem3  38670  mbfresfi  38677  findcard4  38725  mettrifi  38784  opidon2OLD  38881  isexid2  38882  grpomndo  38902  elghomlem2OLD  38913  rngoidmlem  38963  rngoueqz  38967  iscringd  39025  cdlemk35s  42087  cdlemk39s  42089  cdlemk42  42091  uzindd  43121  mzpadd  43842  mzpmul  43843  mzpcompact2  43856  dford3lem2  44127  aomclem6  44154  cnsrexpcl  44260  ensucne0OLD  44624  pr2cv  44642  relexpss1d  44798  iunrelexpmin1  44801  iunrelexpmin2  44805  tfindsd  45301  nzin  45395  axc11next  45483  iotavalsb  45510  ssdec  46196  fperiodmullem  46412  monoordxrv  46584  fmul01  46685  fmulcl  46686  fmuldfeqlem1  46687  fmuldfeq  46688  iblspltprt  47076  itgspltprt  47082  stoweidlem2  47105  stoweidlem3  47106  stoweidlem6  47109  stoweidlem8  47111  stoweidlem17  47120  stoweidlem19  47122  stoweidlem21  47124  stoweidlem26  47129  stoweidlem31  47134  stoweidlem43  47146  fourierdlem42  47252  funressnfv  48206  eu2ndop1stv  48288  afv0fv0  48312  afv0nbfvbi  48314  funressnbrafv2  48407  funbrafv2  48410  nelbrim  48438  ssfz12  48477  smonoord  48540  iccpartiltu  48597  iccpartigtl  48598  iccelpart  48608  icceuelpart  48611  fargshiftf  48615  fargshiftf1  48616  fargshiftfo  48617  sprel  48659  sprsymrelf1lem  48666  sprsymrelfolem2  48668  prproropf1olem4  48681  lighneallem4  48788  mogoldbblem  48911  fpprnn  48921  fpprwppr  48930  fpprwpprb  48931  sbgoldbwt  48968  bgoldbtbndlem2  48997  bgoldbtbndlem4  48999  tgoldbach  49008  grimprop  49074  grlimprop  49175  grilcbri2  49202  upwlkwlk  49330  clcllaw  49381  intop  49393  clintop  49398  assintop  49399  assintopcllaw  49402  lmod0rng  49419  ztprmneprm  49552  scmsuppss  49576  ply1mulgsumlem1  49591  ply1mulgsumlem2  49592  lcoel0  49633  ellcoellss  49640  lindslinindsimp2lem5  49667  ldepspr  49678  flnn0div2ge  49738  nnolog2flm1  49795  blengt1fldiv2p1  49798  dignn0flhalf  49823  naryfvalelfv  49837  0aryfvalelfv  49840  fv1arycl  49842  fv2arycl  49853