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  2440  mo4  2566  sbcn1  3793  sbcim1  3794  sbcbi1  3798  sbcel21v  3808  sbccomlem  3819  csbie2df  4395  elimasni  6050  sotri  6084  unixpid  6242  f0rn0  6719  f1ocnv  6786  funbrfv  6882  elfvmptrab1w  6968  f1dom3el3dif  7215  oprabidw  7389  oprabid  7390  oprabv  7418  ndmovordi  7549  elovmporab  7604  elovmporab1w  7605  elovmporab1  7606  elovmpt3rab1  7618  limomss  7813  unielxp  7971  bropfvvvvlem  8033  f1o2ndf1  8064  smogt  8299  tfrlem1  8307  oawordeulem  8481  omass  8507  ecopovtrn  8757  mapfvd  8817  findcard2d  9091  ssfi  9097  f1domfi  9105  php  9131  unxpdom  9159  findcard3  9183  isfinite2  9198  fsuppimp  9271  fsuppunfi  9291  fsuppunbi  9292  fsuppres  9296  infsupprpr  9409  cantnfval2  9578  cantnfle  9580  cantnfp1lem3  9589  cantnflem1  9598  cnfcom  9609  rankr1ai  9710  rankonidlem  9740  rankxplim2  9792  oncard  9872  ficardom  9873  cardne  9877  acnnum  9962  alephord2i  9987  cardaleph  9999  aceq3lem  10030  dfac5lem5  10037  dfac12lem3  10056  ackbij1lem16  10144  cfslb  10176  cfslb2n  10178  cfsmolem  10180  fin4i  10208  infpssr  10218  fin1a2lem6  10315  axdc3lem2  10361  axcclem  10367  ttukeylem6  10424  fodomb  10436  gchi  10535  pwfseq  10575  inawina  10601  wunfi  10632  inar1  10686  ltexnq  10886  ltbtwnnq  10889  ltexprlem4  10950  ltexpri  10954  prlem936  10958  suplem1pr  10963  suplem2pr  10964  recexsrlem  11014  mulgt0sr  11016  map2psrpr  11021  supsr  11023  eqlei  11243  eqlei2  11244  ledivp1i  12067  nnind  12163  nnmulcl  12169  nn0ge2m1nn  12471  nnnegz  12491  ublbneg  12846  xmulasslem  13200  ixxssixx  13275  iccshftri  13403  iccshftli  13405  iccdili  13407  icccntri  13409  elfz1b  13509  fzo1fzo0n0  13631  elfzonlteqm1  13657  elfzo0l  13672  ssfzo12  13675  fzoopth  13678  elfzo1elm1fzo0  13684  elfzr  13697  elfzlmr  13698  zmodidfzoimp  13821  mptnn0fsuppr  13922  seqp1  13939  seqcl2  13943  seqfveq2  13947  seqshft2  13951  monoord  13955  seqsplit  13958  seqcaopr3  13960  seqf1olem2a  13963  seqf1o  13966  seqid2  13971  seqhomo  13972  hashf1rn  14275  hashinfxadd  14308  hashf1lem2  14379  seqcoll  14387  hash2pr  14392  pr2pwpr  14402  hashge2el2difr  14404  hash3tr  14414  fi1uzind  14430  brfi1indALT  14433  elovmptnn0wrd  14482  swrdswrd  14628  pfxccatin12lem2a  14650  swrdccat  14658  swrdccatin1d  14666  swrdccatin2d  14667  repswccat  14709  cshwidxmod  14726  relexpsucnnr  14948  rtrclreclem3  14983  rtrclreclem4  14984  dfrtrcl2  14985  relexpindlem  14986  relexpind  14987  rtrclind  14988  cjre  15062  climeu  15478  climub  15585  fsum2d  15694  fsumabs  15724  fsumrlim  15734  fsumo1  15735  fsumiun  15744  prodfn0  15817  prodfrec  15818  ntrivcvg  15820  fprodabs  15897  fprod2d  15904  fprodefsum  16018  ruclem9  16163  dvdsmod0  16185  p1modz1  16186  dvdsmodexp  16187  dvdsabseq  16240  mod2eq1n2dvds  16274  mulsucdiv2z  16280  nno  16309  nn0o  16310  sadcadd  16385  sadadd2  16387  saddisjlem  16391  smuval2  16409  smupval  16415  smueqlem  16417  smumullem  16419  dfgcd2  16473  lcmgcdlem  16533  lcmftp  16563  exprmfct  16631  eulerthlem2  16709  dvdsprmpweqnn  16813  dvdsprmpweqle  16814  pcmpt  16820  vdwlem10  16918  cshwsidrepsw  17021  cshwshashlem1  17023  prmlem1a  17034  setsn0fun  17100  ressval3d  17173  mreexexd  17571  letsr  18516  insubm  18743  ghmghmrn  19164  pmtrfrn  19387  pmtr3ncom  19404  gsmtrcl  19445  psgnsn  19449  sylow1lem1  19527  efginvrel2  19656  efgsrel  19663  cntzcmnss  19770  gsum2dlem2  19900  telgsumfzs  19918  dprdval  19934  ablfac1eulem  20003  pgpfac1  20011  pgpfac  20015  srgpcomp  20153  ringrng  20220  ring1ne0  20234  rngimf1o  20390  rngimrnghm  20391  rngimcnv  20392  0ringnnzr  20458  zrhpsgnelbas  21549  psgndiflemA  21556  mplcoe1  21992  mplcoe3  21993  mplcoe5lem  21994  mplcoe5  21995  mpfaddcl  22068  mpfmulcl  22069  coe1ae0  22157  coe1fzgsumd  22248  gsummoncoe1  22252  pf1addcl  22297  pf1mulcl  22298  evl1gsumd  22301  mamufacex  22340  mat0dimcrng  22414  mavmulsolcl  22495  mdetunilem9  22564  cramerlem3  22633  pmatcollpw3fi1  22732  pm2mpfo  22758  chmaidscmat  22792  chfacfscmul0  22802  chfacfpmmul0  22806  cpmadugsumlemF  22820  tg2  22909  neindisj2  23067  neiptopnei  23076  t1t0  23292  fiuncmp  23348  hmeof1o  23708  ist1-5lem  23764  t1r0  23765  alexsublem  23988  imasdsf1olem  24317  tgioo  24740  fsumcn  24817  voliunlem3  25509  itgfsum  25784  dvbsss  25859  dvmptfsum  25935  dvfsumlem2  25989  dvfsumlem2OLD  25990  dvfsumlem4  25992  plyco  26202  dgrcolem1  26235  dgrco  26237  dvntaylp  26335  taylthlem1  26337  jensen  26955  bposlem5  27255  lgsqrmodndvds  27320  gausslemma2dlem0i  27331  gausslemma2dlem4  27336  lgsquad2lem2  27352  2lgslem3  27371  2lgs  27374  2lgsoddprm  27383  dchrisum0flb  27477  pntpbnd1  27553  pntlemf  27572  madebdayim  27884  oldbdayim  27885  pw2cut  28456  brbtwn  28972  brcgr  28973  umgrnloopv  29179  umgrnloop  29181  usgrnloopvALT  29274  usgrnloopALT  29276  usgredg2vlem2  29299  subgrprop  29346  uvtxnbgrvtx  29466  cusgrsize2inds  29527  rgrprop  29634  rusgrprop  29636  wlkprop  29685  wlkvtxeledg  29697  wlkeq  29707  wlkl1loop  29711  wlk1walk  29712  uspgr2wlkeqi  29721  wlkreslem  29741  wlkres  29742  redwlk  29744  lfgrwlknloop  29761  2pthnloop  29804  usgr2trlncl  29833  usgr2pth  29837  clwlkcompim  29853  clwlkcompbp  29855  uspgrn2crct  29881  crctcshwlkn0  29894  wwlknp  29916  wwlkswwlksn  29938  wlkiswwlks2lem4  29945  wlkiswwlks2  29948  wlklnwwlkln2lem  29955  wwlksnext  29966  wwlksnextbi  29967  wwlksnredwwlkn0  29969  wwlksnextwrd  29970  clwlkclwwlklem2a  30073  clwlkclwwlklem2  30075  clwlkclwwlkflem  30079  clwwisshclwws  30090  clwwlknp  30112  clwwlknwwlksn  30113  clwwlkwwlksb  30129  clwwlkext2edg  30131  umgrhashecclwwlk  30153  clwwlknun  30187  1pthond  30219  upgr3v3e3cycl  30255  upgr4cycl4dv4e  30260  eupth2  30314  3vfriswmgr  30353  3cyclfrgrrn1  30360  n4cyclfrgr  30366  frgrnbnb  30368  frgrncvvdeqlem3  30376  frgrncvvdeqlem6  30379  frgrncvvdeqlem7  30380  frgrncvvdeqlem8  30381  frgrwopreglem4a  30385  frgrwopreg  30398  frgrregorufr0  30399  frgr2wwlkeqm  30406  2clwwlk2clwwlklem  30421  wlkl0  30442  frgrreggt1  30468  frgrregord013  30470  frgrregord13  30471  frgrogt3nreg  30472  friendshipgt3  30473  friendship  30474  blocn2  30883  cvexchlem  32443  cdj3lem2b  32512  nnindf  32900  gsumwun  33158  domnprodn0  33357  issgon  34280  sitgclg  34499  sseqp1  34552  bnj938  35093  bnj964  35099  bnj1052  35131  bnj1125  35148  onvf1odlem4  35300  subfacp1lem6  35379  cvmliftlem7  35485  cvmliftlem10  35488  mclsrcl  35755  pprodss4v  36076  segleantisym  36309  rankeq1o  36365  bj-restv  37296  iooelexlt  37563  relowlssretop  37564  rdgeqoa  37571  matunitlindflem1  37813  poimirlem22  37839  poimirlem25  37842  poimirlem28  37845  poimirlem31  37848  mblfinlem3  37856  mbfresfi  37863  mettrifi  37954  opidon2OLD  38051  isexid2  38052  grpomndo  38072  elghomlem2OLD  38083  rngoidmlem  38133  rngoueqz  38137  iscringd  38195  cdlemk35s  41193  cdlemk39s  41195  cdlemk42  41197  uzindd  42227  mzpadd  42976  mzpmul  42977  mzpcompact2  42990  dford3lem2  43265  aomclem6  43297  cnsrexpcl  43403  ensucne0OLD  43767  pr2cv  43785  relexpss1d  43942  iunrelexpmin1  43945  iunrelexpmin2  43949  tfindsd  44447  nzin  44555  axc11next  44643  iotavalsb  44670  ssdec  45328  fperiodmullem  45547  monoordxrv  45721  fmul01  45822  fmulcl  45823  fmuldfeqlem1  45824  fmuldfeq  45825  iblspltprt  46213  itgspltprt  46219  stoweidlem2  46242  stoweidlem3  46243  stoweidlem6  46246  stoweidlem8  46248  stoweidlem17  46257  stoweidlem19  46259  stoweidlem21  46261  stoweidlem26  46266  stoweidlem31  46271  stoweidlem43  46283  fourierdlem42  46389  funressnfv  47285  eu2ndop1stv  47367  afv0fv0  47391  afv0nbfvbi  47393  funressnbrafv2  47486  funbrafv2  47489  nelbrim  47517  ssfz12  47556  smonoord  47613  iccpartiltu  47664  iccpartigtl  47665  iccelpart  47675  icceuelpart  47678  fargshiftf  47682  fargshiftf1  47683  fargshiftfo  47684  sprel  47726  sprsymrelf1lem  47733  sprsymrelfolem2  47735  prproropf1olem4  47748  lighneallem4  47852  mogoldbblem  47962  fpprnn  47972  fpprwppr  47981  fpprwpprb  47982  sbgoldbwt  48019  bgoldbtbndlem2  48048  bgoldbtbndlem4  48050  tgoldbach  48059  grimprop  48125  grlimprop  48226  grilcbri2  48253  upwlkwlk  48381  clcllaw  48433  intop  48445  clintop  48450  assintop  48451  assintopcllaw  48454  lmod0rng  48471  ztprmneprm  48589  scmsuppss  48613  ply1mulgsumlem1  48628  ply1mulgsumlem2  48629  lcoel0  48670  ellcoellss  48677  lindslinindsimp2lem5  48704  ldepspr  48715  flnn0div2ge  48775  nnolog2flm1  48832  blengt1fldiv2p1  48835  dignn0flhalf  48860  naryfvalelfv  48874  0aryfvalelfv  48877  fv1arycl  48879  fv2arycl  48890