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  669  axc16i  2441  mo4  2566  sbcn1  3841  sbcim1  3842  sbcim1OLD  3843  sbcbi1  3847  sbcel21v  3858  sbccomlem  3869  csbie2df  4443  elimasni  6109  sotri  6147  unixpid  6304  f0rn0  6793  f1ocnv  6860  funbrfv  6957  elfvmptrab1w  7043  f1dom3el3dif  7289  oprabidw  7462  oprabid  7463  oprabv  7493  ndmovordi  7624  elovmporab  7679  elovmporab1w  7680  elovmporab1  7681  elovmpt3rab1  7693  limomss  7892  unielxp  8052  bropfvvvvlem  8116  f1o2ndf1  8147  smogt  8407  tfrlem1  8416  oawordeulem  8592  omass  8618  ecopovtrn  8860  mapfvd  8919  findcard2d  9206  ssfi  9213  f1domfi  9221  php  9247  phpOLD  9259  unxpdom  9289  findcard3  9318  findcard3OLD  9319  isfinite2  9334  fsuppimp  9408  fsuppunfi  9428  fsuppunbi  9429  fsuppres  9433  infsupprpr  9544  cantnfval2  9709  cantnfle  9711  cantnfp1lem3  9720  cantnflem1  9729  cnfcom  9740  rankr1ai  9838  rankonidlem  9868  rankxplim2  9920  oncard  10000  ficardom  10001  cardne  10005  acnnum  10092  alephord2i  10117  cardaleph  10129  aceq3lem  10160  dfac5lem5  10167  dfac12lem3  10186  ackbij1lem16  10274  cfslb  10306  cfslb2n  10308  cfsmolem  10310  fin4i  10338  infpssr  10348  fin1a2lem6  10445  axdc3lem2  10491  axcclem  10497  ttukeylem6  10554  fodomb  10566  gchi  10664  pwfseq  10704  inawina  10730  wunfi  10761  inar1  10815  ltexnq  11015  ltbtwnnq  11018  ltexprlem4  11079  ltexpri  11083  prlem936  11087  suplem1pr  11092  suplem2pr  11093  recexsrlem  11143  mulgt0sr  11145  map2psrpr  11150  supsr  11152  eqlei  11371  eqlei2  11372  ledivp1i  12193  nnind  12284  nnmulcl  12290  nn0ge2m1nn  12596  nnnegz  12616  ublbneg  12975  xmulasslem  13327  ixxssixx  13401  iccshftri  13527  iccshftli  13529  iccdili  13531  icccntri  13533  elfz1b  13633  fzo1fzo0n0  13754  elfzonlteqm1  13780  elfzo0l  13795  ssfzo12  13798  fzoopth  13801  elfzo1elm1fzo0  13807  elfzr  13819  elfzlmr  13820  zmodidfzoimp  13941  mptnn0fsuppr  14040  seqp1  14057  seqcl2  14061  seqfveq2  14065  seqshft2  14069  monoord  14073  seqsplit  14076  seqcaopr3  14078  seqf1olem2a  14081  seqf1o  14084  seqid2  14089  seqhomo  14090  hashf1rn  14391  hashinfxadd  14424  hashf1lem2  14495  seqcoll  14503  hash2pr  14508  pr2pwpr  14518  hashge2el2difr  14520  hash3tr  14530  fi1uzind  14546  brfi1indALT  14549  elovmptnn0wrd  14597  swrdswrd  14743  pfxccatin12lem2a  14765  swrdccat  14773  swrdccatin1d  14781  swrdccatin2d  14782  repswccat  14824  cshwidxmod  14841  relexpsucnnr  15064  rtrclreclem3  15099  rtrclreclem4  15100  dfrtrcl2  15101  relexpindlem  15102  relexpind  15103  rtrclind  15104  cjre  15178  climeu  15591  climub  15698  fsum2d  15807  fsumabs  15837  fsumrlim  15847  fsumo1  15848  fsumiun  15857  prodfn0  15930  prodfrec  15931  ntrivcvg  15933  fprodabs  16010  fprod2d  16017  fprodefsum  16131  ruclem9  16274  dvdsmod0  16296  p1modz1  16297  dvdsmodexp  16298  dvdsabseq  16350  mod2eq1n2dvds  16384  mulsucdiv2z  16390  nno  16419  nn0o  16420  sadcadd  16495  sadadd2  16497  saddisjlem  16501  smuval2  16519  smupval  16525  smueqlem  16527  smumullem  16529  dfgcd2  16583  lcmgcdlem  16643  lcmftp  16673  exprmfct  16741  eulerthlem2  16819  dvdsprmpweqnn  16923  dvdsprmpweqle  16924  pcmpt  16930  vdwlem10  17028  cshwsidrepsw  17131  cshwshashlem1  17133  prmlem1a  17144  setsn0fun  17210  ressval3d  17292  mreexexd  17691  letsr  18638  insubm  18831  ghmghmrn  19253  pmtrfrn  19476  pmtr3ncom  19493  gsmtrcl  19534  psgnsn  19538  sylow1lem1  19616  efginvrel2  19745  efgsrel  19752  cntzcmnss  19859  gsum2dlem2  19989  telgsumfzs  20007  dprdval  20023  ablfac1eulem  20092  pgpfac1  20100  pgpfac  20104  srgpcomp  20215  ringrng  20282  ring1ne0  20296  rngimf1o  20454  rngimrnghm  20455  rngimcnv  20456  0ringnnzr  20525  zrhpsgnelbas  21612  psgndiflemA  21619  mplcoe1  22055  mplcoe3  22056  mplcoe5lem  22057  mplcoe5  22058  mpfaddcl  22129  mpfmulcl  22130  coe1ae0  22218  coe1fzgsumd  22308  gsummoncoe1  22312  pf1addcl  22357  pf1mulcl  22358  evl1gsumd  22361  mamufacex  22400  mat0dimcrng  22476  mavmulsolcl  22557  mdetunilem9  22626  cramerlem3  22695  pmatcollpw3fi1  22794  pm2mpfo  22820  chmaidscmat  22854  chfacfscmul0  22864  chfacfpmmul0  22868  cpmadugsumlemF  22882  tg2  22972  neindisj2  23131  neiptopnei  23140  t1t0  23356  fiuncmp  23412  hmeof1o  23772  ist1-5lem  23828  t1r0  23829  alexsublem  24052  imasdsf1olem  24383  tgioo  24817  fsumcn  24894  voliunlem3  25587  itgfsum  25862  dvbsss  25937  dvmptfsum  26013  dvfsumlem2  26067  dvfsumlem2OLD  26068  dvfsumlem4  26070  plyco  26280  dgrcolem1  26313  dgrco  26315  dvntaylp  26413  taylthlem1  26415  jensen  27032  bposlem5  27332  lgsqrmodndvds  27397  gausslemma2dlem0i  27408  gausslemma2dlem4  27413  lgsquad2lem2  27429  2lgslem3  27448  2lgs  27451  2lgsoddprm  27460  dchrisum0flb  27554  pntpbnd1  27630  pntlemf  27649  madebdayim  27926  oldbdayim  27927  pw2cut  28420  brbtwn  28914  brcgr  28915  umgrnloopv  29123  umgrnloop  29125  usgrnloopvALT  29218  usgrnloopALT  29220  usgredg2vlem2  29243  subgrprop  29290  uvtxnbgrvtx  29410  cusgrsize2inds  29471  rgrprop  29578  rusgrprop  29580  wlkprop  29629  wlkvtxeledg  29642  wlkeq  29652  wlkl1loop  29656  wlk1walk  29657  uspgr2wlkeqi  29666  wlkreslem  29687  wlkres  29688  redwlk  29690  lfgrwlknloop  29707  2pthnloop  29751  usgr2trlncl  29780  usgr2pth  29784  clwlkcompim  29800  clwlkcompbp  29802  uspgrn2crct  29828  crctcshwlkn0  29841  wwlknp  29863  wwlkswwlksn  29885  wlkiswwlks2lem4  29892  wlkiswwlks2  29895  wlklnwwlkln2lem  29902  wwlksnext  29913  wwlksnextbi  29914  wwlksnredwwlkn0  29916  wwlksnextwrd  29917  clwlkclwwlklem2a  30017  clwlkclwwlklem2  30019  clwlkclwwlkflem  30023  clwwisshclwws  30034  clwwlknp  30056  clwwlknwwlksn  30057  clwwlkwwlksb  30073  clwwlkext2edg  30075  umgrhashecclwwlk  30097  clwwlknun  30131  1pthond  30163  upgr3v3e3cycl  30199  upgr4cycl4dv4e  30204  eupth2  30258  3vfriswmgr  30297  3cyclfrgrrn1  30304  n4cyclfrgr  30310  frgrnbnb  30312  frgrncvvdeqlem3  30320  frgrncvvdeqlem6  30323  frgrncvvdeqlem7  30324  frgrncvvdeqlem8  30325  frgrwopreglem4a  30329  frgrwopreg  30342  frgrregorufr0  30343  frgr2wwlkeqm  30350  2clwwlk2clwwlklem  30365  wlkl0  30386  frgrreggt1  30412  frgrregord013  30414  frgrregord13  30415  frgrogt3nreg  30416  friendshipgt3  30417  friendship  30418  blocn2  30827  cvexchlem  32387  cdj3lem2b  32456  nnindf  32821  gsumwun  33068  domnprodn0  33279  issgon  34124  sitgclg  34344  sseqp1  34397  bnj938  34951  bnj964  34957  bnj1052  34989  bnj1125  35006  subfacp1lem6  35190  cvmliftlem7  35296  cvmliftlem10  35299  mclsrcl  35566  pprodss4v  35885  segleantisym  36116  rankeq1o  36172  bj-restv  37096  iooelexlt  37363  relowlssretop  37364  rdgeqoa  37371  matunitlindflem1  37623  poimirlem22  37649  poimirlem25  37652  poimirlem28  37655  poimirlem31  37658  mblfinlem3  37666  mbfresfi  37673  mettrifi  37764  opidon2OLD  37861  isexid2  37862  grpomndo  37882  elghomlem2OLD  37893  rngoidmlem  37943  rngoueqz  37947  iscringd  38005  cdlemk35s  40939  cdlemk39s  40941  cdlemk42  40943  uzindd  41978  mzpadd  42749  mzpmul  42750  mzpcompact2  42763  dford3lem2  43039  aomclem6  43071  cnsrexpcl  43177  ensucne0OLD  43543  pr2cv  43561  relexpss1d  43718  iunrelexpmin1  43721  iunrelexpmin2  43725  tfindsd  44224  nzin  44337  axc11next  44425  iotavalsb  44452  ssdec  45093  fperiodmullem  45315  monoordxrv  45492  fmul01  45595  fmulcl  45596  fmuldfeqlem1  45597  fmuldfeq  45598  iblspltprt  45988  itgspltprt  45994  stoweidlem2  46017  stoweidlem3  46018  stoweidlem6  46021  stoweidlem8  46023  stoweidlem17  46032  stoweidlem19  46034  stoweidlem21  46036  stoweidlem26  46041  stoweidlem31  46046  stoweidlem43  46058  fourierdlem42  46164  funressnfv  47055  eu2ndop1stv  47137  afv0fv0  47161  afv0nbfvbi  47163  funressnbrafv2  47256  funbrafv2  47259  nelbrim  47287  ssfz12  47326  smonoord  47358  iccpartiltu  47409  iccpartigtl  47410  iccelpart  47420  icceuelpart  47423  fargshiftf  47427  fargshiftf1  47428  fargshiftfo  47429  sprel  47471  sprsymrelf1lem  47478  sprsymrelfolem2  47480  prproropf1olem4  47493  lighneallem4  47597  mogoldbblem  47707  fpprnn  47717  fpprwppr  47726  fpprwpprb  47727  sbgoldbwt  47764  bgoldbtbndlem2  47793  bgoldbtbndlem4  47795  tgoldbach  47804  grimprop  47869  grlimprop  47951  grilcbri2  47971  upwlkwlk  48055  clcllaw  48107  intop  48119  clintop  48124  assintop  48125  assintopcllaw  48128  lmod0rng  48145  ztprmneprm  48263  scmsuppss  48287  ply1mulgsumlem1  48303  ply1mulgsumlem2  48304  lcoel0  48345  ellcoellss  48352  lindslinindsimp2lem5  48379  ldepspr  48390  flnn0div2ge  48454  nnolog2flm1  48511  blengt1fldiv2p1  48514  dignn0flhalf  48539  naryfvalelfv  48553  0aryfvalelfv  48556  fv1arycl  48558  fv2arycl  48569