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  675  axc16i  2444  mo4  2570  sbcn1  3782  sbcim1  3783  sbcbi1  3787  sbcel21v  3797  sbccomlem  3808  csbie2df  4378  elimasni  6050  sotri  6084  unixpid  6242  f0rn0  6719  f1ocnv  6786  funbrfv  6882  elfvmptrab1w  6970  f1dom3el3dif  7220  oprabidw  7394  oprabid  7395  oprabv  7423  ndmovordi  7554  elovmporab  7609  elovmporab1w  7610  elovmporab1  7611  elovmpt3rab1  7623  limomss  7818  unielxp  7976  bropfvvvvlem  8037  f1o2ndf1  8068  smogt  8304  tfrlem1  8312  oawordeulem  8486  omass  8512  ecopovtrn  8764  mapfvd  8824  findcard2d  9098  ssfi  9104  f1domfi  9112  php  9138  unxpdom  9166  findcard3  9190  isfinite2  9205  fsuppimp  9278  fsuppunfi  9298  fsuppunbi  9299  fsuppres  9303  infsupprpr  9416  cantnfval2  9588  cantnfle  9590  cantnfp1lem3  9599  cantnflem1  9608  cnfcom  9619  rankr1ai  9720  rankonidlem  9750  rankxplim2  9802  oncard  9882  ficardom  9883  cardne  9887  acnnum  9972  alephord2i  9997  cardaleph  10009  aceq3lem  10040  dfac5lem5  10047  dfac12lem3  10066  ackbij1lem16  10154  cfslb  10186  cfslb2n  10188  cfsmolem  10190  fin4i  10218  infpssr  10228  fin1a2lem6  10325  axdc3lem2  10371  axcclem  10377  ttukeylem6  10434  fodomb  10446  gchi  10545  pwfseq  10585  inawina  10611  wunfi  10642  inar1  10696  ltexnq  10896  ltbtwnnq  10899  ltexprlem4  10960  ltexpri  10964  prlem936  10968  suplem1pr  10973  suplem2pr  10974  recexsrlem  11024  mulgt0sr  11026  map2psrpr  11031  supsr  11033  eqlei  11254  eqlei2  11255  ledivp1i  12079  nnind  12190  nnmulcl  12196  nn0ge2m1nn  12505  nnnegz  12525  ublbneg  12881  xmulasslem  13235  ixxssixx  13310  iccshftri  13438  iccshftli  13440  iccdili  13442  icccntri  13444  elfz1b  13545  fzo1fzo0n0  13668  elfzonlteqm1  13694  elfzo0l  13709  ssfzo12  13712  fzoopth  13715  elfzo1elm1fzo0  13721  elfzr  13734  elfzlmr  13735  zmodidfzoimp  13858  mptnn0fsuppr  13959  seqp1  13976  seqcl2  13980  seqfveq2  13984  seqshft2  13988  monoord  13992  seqsplit  13995  seqcaopr3  13997  seqf1olem2a  14000  seqf1o  14003  seqid2  14008  seqhomo  14009  hashf1rn  14312  hashinfxadd  14345  hashf1lem2  14416  seqcoll  14424  hash2pr  14429  pr2pwpr  14439  hashge2el2difr  14441  hash3tr  14451  fi1uzind  14467  brfi1indALT  14470  elovmptnn0wrd  14519  swrdswrd  14665  pfxccatin12lem2a  14687  swrdccat  14695  swrdccatin1d  14703  swrdccatin2d  14704  repswccat  14746  cshwidxmod  14763  relexpsucnnr  14985  rtrclreclem3  15020  rtrclreclem4  15021  dfrtrcl2  15022  relexpindlem  15023  relexpind  15024  rtrclind  15025  cjre  15099  climeu  15515  climub  15622  fsum2d  15731  fsumabs  15762  fsumrlim  15772  fsumo1  15773  fsumiun  15782  prodfn0  15857  prodfrec  15858  ntrivcvg  15860  fprodabs  15937  fprod2d  15944  fprodefsum  16058  ruclem9  16203  dvdsmod0  16225  p1modz1  16226  dvdsmodexp  16227  dvdsabseq  16280  mod2eq1n2dvds  16314  mulsucdiv2z  16320  nno  16349  nn0o  16350  sadcadd  16425  sadadd2  16427  saddisjlem  16431  smuval2  16449  smupval  16455  smueqlem  16457  smumullem  16459  dfgcd2  16513  lcmgcdlem  16573  lcmftp  16603  exprmfct  16672  eulerthlem2  16750  dvdsprmpweqnn  16854  dvdsprmpweqle  16855  pcmpt  16861  vdwlem10  16959  cshwsidrepsw  17062  cshwshashlem1  17064  prmlem1a  17075  setsn0fun  17141  ressval3d  17214  mreexexd  17612  letsr  18557  insubm  18784  ghmghmrn  19208  pmtrfrn  19431  pmtr3ncom  19448  gsmtrcl  19489  psgnsn  19493  sylow1lem1  19571  efginvrel2  19700  efgsrel  19707  cntzcmnss  19814  gsum2dlem2  19944  telgsumfzs  19962  dprdval  19978  ablfac1eulem  20047  pgpfac1  20055  pgpfac  20059  srgpcomp  20197  ringrng  20264  ring1ne0  20278  rngimf1o  20432  rngimrnghm  20433  rngimcnv  20434  0ringnnzr  20504  zrhpsgnelbas  21576  psgndiflemA  21583  mplcoe1  22020  mplcoe3  22021  mplcoe5lem  22022  mplcoe5  22023  mpfaddcl  22096  mpfmulcl  22097  coe1ae0  22208  coe1fzgsumd  22297  gsummoncoe1  22301  pf1addcl  22346  pf1mulcl  22347  evl1gsumd  22350  mamufacex  22386  mat0dimcrng  22460  mavmulsolcl  22541  mdetunilem9  22610  cramerlem3  22679  pmatcollpw3fi1  22778  pm2mpfo  22804  chmaidscmat  22838  chfacfscmul0  22848  chfacfpmmul0  22852  cpmadugsumlemF  22866  tg2  22955  neindisj2  23113  neiptopnei  23122  t1t0  23338  fiuncmp  23394  hmeof1o  23754  ist1-5lem  23810  t1r0  23811  alexsublem  24034  imasdsf1olem  24363  tgioo  24786  fsumcn  24862  voliunlem3  25544  itgfsum  25819  dvbsss  25894  dvmptfsum  25967  dvfsumlem2  26019  dvfsumlem4  26021  plyco  26231  dgrcolem1  26263  dgrco  26265  dvntaylp  26361  taylthlem1  26363  jensen  26977  bposlem5  27276  lgsqrmodndvds  27341  gausslemma2dlem0i  27352  gausslemma2dlem4  27357  lgsquad2lem2  27373  2lgslem3  27392  2lgs  27395  2lgsoddprm  27404  dchrisum0flb  27498  pntpbnd1  27574  pntlemf  27593  madebdayim  27905  oldbdayim  27906  pw2cut  28477  brbtwn  28993  brcgr  28994  umgrnloopv  29200  umgrnloop  29202  usgrnloopvALT  29295  usgrnloopALT  29297  usgredg2vlem2  29320  subgrprop  29367  uvtxnbgrvtx  29487  cusgrsize2inds  29547  rgrprop  29654  rusgrprop  29656  wlkprop  29705  wlkvtxeledg  29717  wlkeq  29727  wlkl1loop  29731  wlk1walk  29732  uspgr2wlkeqi  29741  wlkreslem  29761  wlkres  29762  redwlk  29764  lfgrwlknloop  29781  2pthnloop  29824  usgr2trlncl  29853  usgr2pth  29857  clwlkcompim  29873  clwlkcompbp  29875  uspgrn2crct  29901  crctcshwlkn0  29914  wwlknp  29936  wwlkswwlksn  29958  wlkiswwlks2lem4  29965  wlkiswwlks2  29968  wlklnwwlkln2lem  29975  wwlksnext  29986  wwlksnextbi  29987  wwlksnredwwlkn0  29989  wwlksnextwrd  29990  clwlkclwwlklem2a  30093  clwlkclwwlklem2  30095  clwlkclwwlkflem  30099  clwwisshclwws  30110  clwwlknp  30132  clwwlknwwlksn  30133  clwwlkwwlksb  30149  clwwlkext2edg  30151  umgrhashecclwwlk  30173  clwwlknun  30207  1pthond  30239  upgr3v3e3cycl  30275  upgr4cycl4dv4e  30280  eupth2  30334  3vfriswmgr  30373  3cyclfrgrrn1  30380  n4cyclfrgr  30386  frgrnbnb  30388  frgrncvvdeqlem3  30396  frgrncvvdeqlem6  30399  frgrncvvdeqlem7  30400  frgrncvvdeqlem8  30401  frgrwopreglem4a  30405  frgrwopreg  30418  frgrregorufr0  30419  frgr2wwlkeqm  30426  2clwwlk2clwwlklem  30441  wlkl0  30462  frgrreggt1  30488  frgrregord013  30490  frgrregord13  30491  frgrogt3nreg  30492  friendshipgt3  30493  friendship  30494  blocn2  30904  cvexchlem  32464  cdj3lem2b  32533  nnindf  32919  gsumwun  33164  domnprodn0  33363  issgon  34314  sitgclg  34533  sseqp1  34586  bnj938  35126  bnj964  35132  bnj1052  35164  bnj1125  35181  onvf1odlem4  35341  subfacp1lem6  35420  cvmliftlem7  35526  cvmliftlem10  35529  mclsrcl  35796  pprodss4v  36117  segleantisym  36350  rankeq1o  36406  bj-restv  37460  iooelexlt  37731  relowlssretop  37732  rdgeqoa  37739  matunitlindflem1  37990  poimirlem22  38016  poimirlem25  38019  poimirlem28  38022  poimirlem31  38025  mblfinlem3  38033  mbfresfi  38040  mettrifi  38131  opidon2OLD  38228  isexid2  38229  grpomndo  38249  elghomlem2OLD  38260  rngoidmlem  38310  rngoueqz  38314  iscringd  38372  cdlemk35s  41436  cdlemk39s  41438  cdlemk42  41440  uzindd  42470  mzpadd  43194  mzpmul  43195  mzpcompact2  43208  dford3lem2  43479  aomclem6  43511  cnsrexpcl  43617  ensucne0OLD  43981  pr2cv  43999  relexpss1d  44156  iunrelexpmin1  44159  iunrelexpmin2  44163  tfindsd  44661  nzin  44769  axc11next  44857  iotavalsb  44884  ssdec  45542  fperiodmullem  45758  monoordxrv  45931  fmul01  46032  fmulcl  46033  fmuldfeqlem1  46034  fmuldfeq  46035  iblspltprt  46423  itgspltprt  46429  stoweidlem2  46452  stoweidlem3  46453  stoweidlem6  46456  stoweidlem8  46458  stoweidlem17  46467  stoweidlem19  46469  stoweidlem21  46471  stoweidlem26  46476  stoweidlem31  46481  stoweidlem43  46493  fourierdlem42  46599  funressnfv  47513  eu2ndop1stv  47595  afv0fv0  47619  afv0nbfvbi  47621  funressnbrafv2  47714  funbrafv2  47717  nelbrim  47745  ssfz12  47784  smonoord  47847  iccpartiltu  47904  iccpartigtl  47905  iccelpart  47915  icceuelpart  47918  fargshiftf  47922  fargshiftf1  47923  fargshiftfo  47924  sprel  47966  sprsymrelf1lem  47973  sprsymrelfolem2  47975  prproropf1olem4  47988  lighneallem4  48095  mogoldbblem  48218  fpprnn  48228  fpprwppr  48237  fpprwpprb  48238  sbgoldbwt  48275  bgoldbtbndlem2  48304  bgoldbtbndlem4  48306  tgoldbach  48315  grimprop  48381  grlimprop  48482  grilcbri2  48509  upwlkwlk  48637  clcllaw  48689  intop  48701  clintop  48706  assintop  48707  assintopcllaw  48710  lmod0rng  48727  ztprmneprm  48845  scmsuppss  48869  ply1mulgsumlem1  48884  ply1mulgsumlem2  48885  lcoel0  48926  ellcoellss  48933  lindslinindsimp2lem5  48960  ldepspr  48971  flnn0div2ge  49031  nnolog2flm1  49088  blengt1fldiv2p1  49091  dignn0flhalf  49116  naryfvalelfv  49130  0aryfvalelfv  49133  fv1arycl  49135  fv2arycl  49146