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  667  axc16i  2458  mo4  2650  sbcn1  3824  sbcim1  3825  sbcbi1  3830  sbcel21v  3842  csbie2df  4392  elimasni  5956  sotri  5987  unixpid  6135  f0rn0  6564  f1ocnv  6627  funbrfv  6716  elfvmptrab1w  6794  f1dom3el3dif  7027  oprabidw  7187  oprabid  7188  oprabv  7214  ndmovordi  7339  elovmporab  7391  elovmporab1w  7392  elovmporab1  7393  elovmpt3rab1  7405  limomss  7585  unielxp  7727  bropfvvvvlem  7786  f1o2ndf1  7818  smogt  8004  tfrlem1  8012  oawordeulem  8180  omass  8206  ecopovtrn  8400  mapfvd  8443  php  8701  unxpdom  8725  findcard2d  8760  findcard3  8761  isfinite2  8776  fsuppimp  8839  fsuppunfi  8853  fsuppunbi  8854  fsuppres  8858  infsupprpr  8968  cantnfval2  9132  cantnfle  9134  cantnfp1lem3  9143  cantnflem1  9152  cnfcom  9163  rankr1ai  9227  rankonidlem  9257  rankxplim2  9309  oncard  9389  ficardom  9390  cardne  9394  acnnum  9478  alephord2i  9503  cardaleph  9515  aceq3lem  9546  dfac5lem5  9553  dfac12lem3  9571  ackbij1lem16  9657  cfslb  9688  cfslb2n  9690  cfsmolem  9692  fin4i  9720  infpssr  9730  fin1a2lem6  9827  axdc3lem2  9873  axcclem  9879  ttukeylem6  9936  fodomb  9948  gchi  10046  fpwwe2lem5  10056  pwfseqlem4  10084  pwfseq  10086  inawina  10112  wunfi  10143  inar1  10197  ltexnq  10397  ltbtwnnq  10400  ltexprlem4  10461  ltexpri  10465  prlem936  10469  suplem1pr  10474  suplem2pr  10475  recexsrlem  10525  mulgt0sr  10527  map2psrpr  10532  supsr  10534  eqlei  10750  eqlei2  10751  ledivp1i  11565  nnind  11656  nnmulcl  11662  nn0ge2m1nn  11965  nnnegz  11985  ublbneg  12334  xmulasslem  12679  ixxssixx  12753  iccshftri  12874  iccshftli  12876  iccdili  12878  icccntri  12880  elfz1b  12977  fzo1fzo0n0  13089  elfzonlteqm1  13114  elfzo0l  13128  ssfzo12  13131  elfzo1elm1fzo0  13139  elfzr  13151  elfzlmr  13152  zmodidfzoimp  13270  mptnn0fsuppr  13368  seqp1  13385  seqcl2  13389  seqfveq2  13393  seqshft2  13397  monoord  13401  seqsplit  13404  seqcaopr3  13406  seqf1olem2a  13409  seqf1o  13412  seqid2  13417  seqhomo  13418  hashf1rn  13714  hashinfxadd  13747  hashf1lem2  13815  seqcoll  13823  hash2pr  13828  pr2pwpr  13838  hashge2el2difr  13840  hash3tr  13849  fi1uzind  13856  brfi1indALT  13859  elovmptnn0wrd  13911  swrdswrd  14067  pfxccatin12lem2a  14089  swrdccat  14097  swrdccatin1d  14105  swrdccatin2d  14106  repswccat  14148  cshwidxmod  14165  relexpsucnnr  14384  rtrclreclem3  14419  rtrclreclem4  14420  dfrtrcl2  14421  relexpindlem  14422  relexpind  14423  rtrclind  14424  cjre  14498  climeu  14912  climub  15018  fsum2d  15126  fsumabs  15156  fsumrlim  15166  fsumo1  15167  fsumiun  15176  prodfn0  15250  prodfrec  15251  ntrivcvg  15253  fprodabs  15328  fprod2d  15335  fprodefsum  15448  ruclem9  15591  dvdsmod0  15613  p1modz1  15614  dvdsmodexp  15615  dvdsabseq  15663  mod2eq1n2dvds  15696  mulsucdiv2z  15702  nno  15733  nn0o  15734  sadcadd  15807  sadadd2  15809  saddisjlem  15813  smuval2  15831  smupval  15837  smueqlem  15839  smumullem  15841  dfgcd2  15894  lcmgcdlem  15950  lcmftp  15980  exprmfct  16048  eulerthlem2  16119  dvdsprmpweqnn  16221  dvdsprmpweqle  16222  pcmpt  16228  vdwlem10  16326  cshwsidrepsw  16427  cshwshashlem1  16429  prmlem1a  16440  setsn0fun  16520  ressval3d  16561  mreexexd  16919  letsr  17837  insubm  17983  ghmghmrn  18377  pmtrfrn  18586  pmtr3ncom  18603  gsmtrcl  18644  psgnsn  18648  sylow1lem1  18723  efginvrel2  18853  efgsrel  18860  cntzcmnss  18961  gsum2dlem2  19091  telgsumfzs  19109  dprdval  19125  ablfac1eulem  19194  pgpfac1  19202  pgpfac  19206  srgpcomp  19282  ring1ne0  19341  rimf1o  19486  rimrhm  19487  brric2  19500  0ringnnzr  20042  mplcoe1  20246  mplcoe3  20247  mplcoe5lem  20248  mplcoe5  20249  mpfaddcl  20318  mpfmulcl  20319  coe1ae0  20384  coe1fzgsumd  20470  gsummoncoe1  20472  pf1addcl  20516  pf1mulcl  20517  evl1gsumd  20520  zrhpsgnelbas  20738  psgndiflemA  20745  mamufacex  21000  mat0dimcrng  21079  mavmulsolcl  21160  mdetunilem9  21229  cramerlem3  21298  pmatcollpw3fi1  21396  pm2mpfo  21422  chmaidscmat  21456  chfacfscmul0  21466  chfacfpmmul0  21470  cpmadugsumlemF  21484  tg2  21573  neindisj2  21731  neiptopnei  21740  t1t0  21956  fiuncmp  22012  hmeof1o  22372  ist1-5lem  22428  t1r0  22429  alexsublem  22652  imasdsf1olem  22983  tgioo  23404  fsumcn  23478  voliunlem3  24153  itgfsum  24427  dvbsss  24500  dvmptfsum  24572  dvfsumlem2  24624  dvfsumlem4  24626  plyco  24831  dgrcolem1  24863  dgrco  24865  dvntaylp  24959  taylthlem1  24961  jensen  25566  bposlem5  25864  lgsqrmodndvds  25929  gausslemma2dlem0i  25940  gausslemma2dlem4  25945  lgsquad2lem2  25961  2lgslem3  25980  2lgs  25983  2lgsoddprm  25992  dchrisum0flb  26086  pntpbnd1  26162  pntlemf  26181  brbtwn  26685  brcgr  26686  umgrnloopv  26891  umgrnloop  26893  usgrnloopvALT  26983  usgrnloopALT  26985  usgredg2vlem2  27008  subgrprop  27055  uvtxnbgrvtx  27175  cusgrsize2inds  27235  rgrprop  27342  rusgrprop  27344  wlkprop  27393  wlkvtxeledg  27405  wlkeq  27415  wlkl1loop  27419  wlk1walk  27420  uspgr2wlkeqi  27429  wlkreslem  27451  wlkres  27452  redwlk  27454  lfgrwlknloop  27471  2pthnloop  27512  usgr2trlncl  27541  usgr2pth  27545  clwlkcompim  27561  clwlkcompbp  27563  uspgrn2crct  27586  crctcshwlkn0  27599  wwlknp  27621  wwlkswwlksn  27643  wlkiswwlks2lem4  27650  wlkiswwlks2  27653  wlklnwwlkln2lem  27660  wwlksnext  27671  wwlksnextbi  27672  wwlksnredwwlkn0  27674  wwlksnextwrd  27675  clwlkclwwlklem2a  27776  clwlkclwwlklem2  27778  clwlkclwwlkflem  27782  clwwisshclwws  27793  clwwlknp  27815  clwwlknwwlksn  27816  clwwlkwwlksb  27833  clwwlkext2edg  27835  umgrhashecclwwlk  27857  clwwlknun  27891  1pthond  27923  upgr3v3e3cycl  27959  upgr4cycl4dv4e  27964  eupth2  28018  3vfriswmgr  28057  3cyclfrgrrn1  28064  n4cyclfrgr  28070  frgrnbnb  28072  frgrncvvdeqlem3  28080  frgrncvvdeqlem6  28083  frgrncvvdeqlem7  28084  frgrncvvdeqlem8  28085  frgrwopreglem4a  28089  frgrwopreg  28102  frgrregorufr0  28103  frgr2wwlkeqm  28110  2clwwlk2clwwlklem  28125  wlkl0  28146  frgrreggt1  28172  frgrregord013  28174  frgrregord13  28175  frgrogt3nreg  28176  friendshipgt3  28177  friendship  28178  blocn2  28585  cvexchlem  30145  cdj3lem2b  30214  cnvoprabOLD  30456  nnindf  30535  issgon  31382  sitgclg  31600  sseqp1  31653  bnj938  32209  bnj964  32215  bnj1052  32247  bnj1125  32264  subfacp1lem6  32432  cvmliftlem7  32538  cvmliftlem10  32541  mclsrcl  32808  pprodss4v  33345  segleantisym  33576  rankeq1o  33632  bj-restv  34389  iooelexlt  34646  relowlssretop  34647  rdgeqoa  34654  matunitlindflem1  34903  poimirlem22  34929  poimirlem25  34932  poimirlem28  34935  poimirlem31  34938  mblfinlem3  34946  mbfresfi  34953  mettrifi  35047  opidon2OLD  35147  isexid2  35148  grpomndo  35168  elghomlem2OLD  35179  rngoidmlem  35229  rngoueqz  35233  iscringd  35291  cdlemk35s  38088  cdlemk39s  38090  cdlemk42  38092  mzpadd  39384  mzpmul  39385  mzpcompact2  39398  dford3lem2  39673  aomclem6  39708  cnsrexpcl  39814  ensucne0OLD  39945  pr2cv  39956  relexpss1d  40099  iunrelexpmin1  40102  iunrelexpmin2  40106  tfindsd  40613  nzin  40699  axc11next  40787  iotavalsb  40814  ssdec  41403  fperiodmullem  41619  monoordxrv  41807  fmul01  41910  fmulcl  41911  fmuldfeqlem1  41912  fmuldfeq  41913  fprodcnlem  41929  iblspltprt  42307  itgspltprt  42313  stoweidlem2  42336  stoweidlem3  42337  stoweidlem6  42340  stoweidlem8  42342  stoweidlem17  42351  stoweidlem19  42353  stoweidlem21  42355  stoweidlem26  42360  stoweidlem31  42365  stoweidlem43  42377  fourierdlem42  42483  funressnfv  43327  eu2ndop1stv  43373  afv0fv0  43397  afv0nbfvbi  43399  funressnbrafv2  43492  funbrafv2  43495  nelbrim  43523  ssfz12  43563  fzoopth  43576  smonoord  43580  iccpartiltu  43631  iccpartigtl  43632  iccelpart  43642  icceuelpart  43645  fargshiftf  43649  fargshiftf1  43650  fargshiftfo  43651  sprel  43695  sprsymrelf1lem  43702  sprsymrelfolem2  43704  prproropf1olem4  43717  lighneallem4  43824  mogoldbblem  43934  fpprnn  43944  fpprwppr  43953  fpprwpprb  43954  sbgoldbwt  43991  bgoldbtbndlem2  44020  bgoldbtbndlem4  44022  tgoldbach  44031  upwlkwlk  44063  clcllaw  44147  intop  44159  clintop  44164  assintop  44165  assintopcllaw  44168  lmod0rng  44188  ringrng  44199  rngimf1o  44225  rngimrnghm  44226  ztprmneprm  44444  scmsuppss  44469  ply1mulgsumlem1  44489  ply1mulgsumlem2  44490  lcoel0  44532  ellcoellss  44539  lindslinindsimp2lem5  44566  ldepspr  44577  flnn0div2ge  44642  nnolog2flm1  44699  blengt1fldiv2p1  44702  dignn0flhalf  44727