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:  anabsi5  668  axc16i  2436  mo4  2561  sbcn1  3833  sbcim1  3834  sbcim1OLD  3835  sbcbi1  3839  sbcel21v  3851  csbie2df  4441  elimasni  6091  sotri  6129  unixpid  6284  f0rn0  6777  f1ocnv  6846  funbrfv  6943  elfvmptrab1w  7025  f1dom3el3dif  7268  oprabidw  7440  oprabid  7441  oprabv  7469  ndmovordi  7598  elovmporab  7652  elovmporab1w  7653  elovmporab1  7654  elovmpt3rab1  7666  limomss  7860  unielxp  8013  bropfvvvvlem  8077  f1o2ndf1  8108  smogt  8367  tfrlem1  8376  oawordeulem  8554  omass  8580  ecopovtrn  8814  mapfvd  8873  findcard2d  9166  ssfi  9173  f1domfi  9184  php  9210  phpOLD  9222  unxpdom  9253  findcard3  9285  findcard3OLD  9286  isfinite2  9301  fsuppimp  9368  fsuppunfi  9383  fsuppunbi  9384  fsuppres  9388  infsupprpr  9499  cantnfval2  9664  cantnfle  9666  cantnfp1lem3  9675  cantnflem1  9684  cnfcom  9695  rankr1ai  9793  rankonidlem  9823  rankxplim2  9875  oncard  9955  ficardom  9956  cardne  9960  acnnum  10047  alephord2i  10072  cardaleph  10084  aceq3lem  10115  dfac5lem5  10122  dfac12lem3  10140  ackbij1lem16  10230  cfslb  10261  cfslb2n  10263  cfsmolem  10265  fin4i  10293  infpssr  10303  fin1a2lem6  10400  axdc3lem2  10446  axcclem  10452  ttukeylem6  10509  fodomb  10521  gchi  10619  fpwwe2lem4  10629  pwfseqlem4  10657  pwfseq  10659  inawina  10685  wunfi  10716  inar1  10770  ltexnq  10970  ltbtwnnq  10973  ltexprlem4  11034  ltexpri  11038  prlem936  11042  suplem1pr  11047  suplem2pr  11048  recexsrlem  11098  mulgt0sr  11100  map2psrpr  11105  supsr  11107  eqlei  11324  eqlei2  11325  ledivp1i  12139  nnind  12230  nnmulcl  12236  nn0ge2m1nn  12541  nnnegz  12561  ublbneg  12917  xmulasslem  13264  ixxssixx  13338  iccshftri  13464  iccshftli  13466  iccdili  13468  icccntri  13470  elfz1b  13570  fzo1fzo0n0  13683  elfzonlteqm1  13708  elfzo0l  13722  ssfzo12  13725  elfzo1elm1fzo0  13733  elfzr  13745  elfzlmr  13746  zmodidfzoimp  13866  mptnn0fsuppr  13964  seqp1  13981  seqcl2  13986  seqfveq2  13990  seqshft2  13994  monoord  13998  seqsplit  14001  seqcaopr3  14003  seqf1olem2a  14006  seqf1o  14009  seqid2  14014  seqhomo  14015  hashf1rn  14312  hashinfxadd  14345  hashf1lem2  14417  seqcoll  14425  hash2pr  14430  pr2pwpr  14440  hashge2el2difr  14442  hash3tr  14451  fi1uzind  14458  brfi1indALT  14461  elovmptnn0wrd  14509  swrdswrd  14655  pfxccatin12lem2a  14677  swrdccat  14685  swrdccatin1d  14693  swrdccatin2d  14694  repswccat  14736  cshwidxmod  14753  relexpsucnnr  14972  rtrclreclem3  15007  rtrclreclem4  15008  dfrtrcl2  15009  relexpindlem  15010  relexpind  15011  rtrclind  15012  cjre  15086  climeu  15499  climub  15608  fsum2d  15717  fsumabs  15747  fsumrlim  15757  fsumo1  15758  fsumiun  15767  prodfn0  15840  prodfrec  15841  ntrivcvg  15843  fprodabs  15918  fprod2d  15925  fprodefsum  16038  ruclem9  16181  dvdsmod0  16203  p1modz1  16204  dvdsmodexp  16205  dvdsabseq  16256  mod2eq1n2dvds  16290  mulsucdiv2z  16296  nno  16325  nn0o  16326  sadcadd  16399  sadadd2  16401  saddisjlem  16405  smuval2  16423  smupval  16429  smueqlem  16431  smumullem  16433  dfgcd2  16488  lcmgcdlem  16543  lcmftp  16573  exprmfct  16641  eulerthlem2  16715  dvdsprmpweqnn  16818  dvdsprmpweqle  16819  pcmpt  16825  vdwlem10  16923  cshwsidrepsw  17027  cshwshashlem1  17029  prmlem1a  17040  setsn0fun  17106  ressval3d  17191  ressval3dOLD  17192  mreexexd  17592  letsr  18546  insubm  18699  ghmghmrn  19111  pmtrfrn  19326  pmtr3ncom  19343  gsmtrcl  19384  psgnsn  19388  sylow1lem1  19466  efginvrel2  19595  efgsrel  19602  cntzcmnss  19709  gsum2dlem2  19839  telgsumfzs  19857  dprdval  19873  ablfac1eulem  19942  pgpfac1  19950  pgpfac  19954  srgpcomp  20041  ring1ne0  20111  0ringnnzr  20302  zrhpsgnelbas  21147  psgndiflemA  21154  mplcoe1  21592  mplcoe3  21593  mplcoe5lem  21594  mplcoe5  21595  mpfaddcl  21668  mpfmulcl  21669  coe1ae0  21740  coe1fzgsumd  21826  gsummoncoe1  21828  pf1addcl  21872  pf1mulcl  21873  evl1gsumd  21876  mamufacex  21891  mat0dimcrng  21972  mavmulsolcl  22053  mdetunilem9  22122  cramerlem3  22191  pmatcollpw3fi1  22290  pm2mpfo  22316  chmaidscmat  22350  chfacfscmul0  22360  chfacfpmmul0  22364  cpmadugsumlemF  22378  tg2  22468  neindisj2  22627  neiptopnei  22636  t1t0  22852  fiuncmp  22908  hmeof1o  23268  ist1-5lem  23324  t1r0  23325  alexsublem  23548  imasdsf1olem  23879  tgioo  24312  fsumcn  24386  voliunlem3  25069  itgfsum  25344  dvbsss  25419  dvmptfsum  25492  dvfsumlem2  25544  dvfsumlem4  25546  plyco  25755  dgrcolem1  25787  dgrco  25789  dvntaylp  25883  taylthlem1  25885  jensen  26493  bposlem5  26791  lgsqrmodndvds  26856  gausslemma2dlem0i  26867  gausslemma2dlem4  26872  lgsquad2lem2  26888  2lgslem3  26907  2lgs  26910  2lgsoddprm  26919  dchrisum0flb  27013  pntpbnd1  27089  pntlemf  27108  madebdayim  27382  oldbdayim  27383  brbtwn  28157  brcgr  28158  umgrnloopv  28366  umgrnloop  28368  usgrnloopvALT  28458  usgrnloopALT  28460  usgredg2vlem2  28483  subgrprop  28530  uvtxnbgrvtx  28650  cusgrsize2inds  28710  rgrprop  28817  rusgrprop  28819  wlkprop  28868  wlkvtxeledg  28881  wlkeq  28891  wlkl1loop  28895  wlk1walk  28896  uspgr2wlkeqi  28905  wlkreslem  28926  wlkres  28927  redwlk  28929  lfgrwlknloop  28946  2pthnloop  28988  usgr2trlncl  29017  usgr2pth  29021  clwlkcompim  29037  clwlkcompbp  29039  uspgrn2crct  29062  crctcshwlkn0  29075  wwlknp  29097  wwlkswwlksn  29119  wlkiswwlks2lem4  29126  wlkiswwlks2  29129  wlklnwwlkln2lem  29136  wwlksnext  29147  wwlksnextbi  29148  wwlksnredwwlkn0  29150  wwlksnextwrd  29151  clwlkclwwlklem2a  29251  clwlkclwwlklem2  29253  clwlkclwwlkflem  29257  clwwisshclwws  29268  clwwlknp  29290  clwwlknwwlksn  29291  clwwlkwwlksb  29307  clwwlkext2edg  29309  umgrhashecclwwlk  29331  clwwlknun  29365  1pthond  29397  upgr3v3e3cycl  29433  upgr4cycl4dv4e  29438  eupth2  29492  3vfriswmgr  29531  3cyclfrgrrn1  29538  n4cyclfrgr  29544  frgrnbnb  29546  frgrncvvdeqlem3  29554  frgrncvvdeqlem6  29557  frgrncvvdeqlem7  29558  frgrncvvdeqlem8  29559  frgrwopreglem4a  29563  frgrwopreg  29576  frgrregorufr0  29577  frgr2wwlkeqm  29584  2clwwlk2clwwlklem  29599  wlkl0  29620  frgrreggt1  29646  frgrregord013  29648  frgrregord13  29649  frgrogt3nreg  29650  friendshipgt3  29651  friendship  29652  blocn2  30061  cvexchlem  31621  cdj3lem2b  31690  cnvoprabOLD  31945  nnindf  32025  issgon  33121  sitgclg  33341  sseqp1  33394  bnj938  33948  bnj964  33954  bnj1052  33986  bnj1125  34003  subfacp1lem6  34176  cvmliftlem7  34282  cvmliftlem10  34285  mclsrcl  34552  pprodss4v  34856  segleantisym  35087  rankeq1o  35143  gg-dvfsumlem2  35183  bj-restv  35976  iooelexlt  36243  relowlssretop  36244  rdgeqoa  36251  matunitlindflem1  36484  poimirlem22  36510  poimirlem25  36513  poimirlem28  36516  poimirlem31  36519  mblfinlem3  36527  mbfresfi  36534  mettrifi  36625  opidon2OLD  36722  isexid2  36723  grpomndo  36743  elghomlem2OLD  36754  rngoidmlem  36804  rngoueqz  36808  iscringd  36866  cdlemk35s  39808  cdlemk39s  39810  cdlemk42  39812  uzindd  40842  mzpadd  41476  mzpmul  41477  mzpcompact2  41490  dford3lem2  41766  aomclem6  41801  cnsrexpcl  41907  ensucne0OLD  42281  pr2cv  42299  relexpss1d  42456  iunrelexpmin1  42459  iunrelexpmin2  42463  tfindsd  42964  nzin  43077  axc11next  43165  iotavalsb  43192  ssdec  43777  fperiodmullem  44013  monoordxrv  44192  fmul01  44296  fmulcl  44297  fmuldfeqlem1  44298  fmuldfeq  44299  fprodcnlem  44315  iblspltprt  44689  itgspltprt  44695  stoweidlem2  44718  stoweidlem3  44719  stoweidlem6  44722  stoweidlem8  44724  stoweidlem17  44733  stoweidlem19  44735  stoweidlem21  44737  stoweidlem26  44742  stoweidlem31  44747  stoweidlem43  44759  fourierdlem42  44865  funressnfv  45753  eu2ndop1stv  45833  afv0fv0  45857  afv0nbfvbi  45859  funressnbrafv2  45952  funbrafv2  45955  nelbrim  45983  ssfz12  46022  fzoopth  46035  smonoord  46039  iccpartiltu  46090  iccpartigtl  46091  iccelpart  46101  icceuelpart  46104  fargshiftf  46108  fargshiftf1  46109  fargshiftfo  46110  sprel  46152  sprsymrelf1lem  46159  sprsymrelfolem2  46161  prproropf1olem4  46174  lighneallem4  46278  mogoldbblem  46388  fpprnn  46398  fpprwppr  46407  fpprwpprb  46408  sbgoldbwt  46445  bgoldbtbndlem2  46474  bgoldbtbndlem4  46476  tgoldbach  46485  upwlkwlk  46517  clcllaw  46601  intop  46613  clintop  46618  assintop  46619  assintopcllaw  46622  lmod0rng  46642  ringrng  46655  rngimf1o  46703  rngimrnghm  46704  rngimcnv  46705  ztprmneprm  47023  scmsuppss  47048  ply1mulgsumlem1  47067  ply1mulgsumlem2  47068  lcoel0  47109  ellcoellss  47116  lindslinindsimp2lem5  47143  ldepspr  47154  flnn0div2ge  47219  nnolog2flm1  47276  blengt1fldiv2p1  47279  dignn0flhalf  47304  naryfvalelfv  47318  0aryfvalelfv  47321  fv1arycl  47323  fv2arycl  47334