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  2436  mo4  2561  sbcn1  3794  sbcim1  3795  sbcbi1  3799  sbcel21v  3809  sbccomlem  3820  csbie2df  4393  elimasni  6040  sotri  6074  unixpid  6231  f0rn0  6708  f1ocnv  6775  funbrfv  6870  elfvmptrab1w  6956  f1dom3el3dif  7203  oprabidw  7377  oprabid  7378  oprabv  7406  ndmovordi  7537  elovmporab  7592  elovmporab1w  7593  elovmporab1  7594  elovmpt3rab1  7606  limomss  7801  unielxp  7959  bropfvvvvlem  8021  f1o2ndf1  8052  smogt  8287  tfrlem1  8295  oawordeulem  8469  omass  8495  ecopovtrn  8744  mapfvd  8803  findcard2d  9076  ssfi  9082  f1domfi  9090  php  9116  unxpdom  9143  findcard3  9167  isfinite2  9182  fsuppimp  9252  fsuppunfi  9272  fsuppunbi  9273  fsuppres  9277  infsupprpr  9390  cantnfval2  9559  cantnfle  9561  cantnfp1lem3  9570  cantnflem1  9579  cnfcom  9590  rankr1ai  9688  rankonidlem  9718  rankxplim2  9770  oncard  9850  ficardom  9851  cardne  9855  acnnum  9940  alephord2i  9965  cardaleph  9977  aceq3lem  10008  dfac5lem5  10015  dfac12lem3  10034  ackbij1lem16  10122  cfslb  10154  cfslb2n  10156  cfsmolem  10158  fin4i  10186  infpssr  10196  fin1a2lem6  10293  axdc3lem2  10339  axcclem  10345  ttukeylem6  10402  fodomb  10414  gchi  10512  pwfseq  10552  inawina  10578  wunfi  10609  inar1  10663  ltexnq  10863  ltbtwnnq  10866  ltexprlem4  10927  ltexpri  10931  prlem936  10935  suplem1pr  10940  suplem2pr  10941  recexsrlem  10991  mulgt0sr  10993  map2psrpr  10998  supsr  11000  eqlei  11220  eqlei2  11221  ledivp1i  12044  nnind  12140  nnmulcl  12146  nn0ge2m1nn  12448  nnnegz  12468  ublbneg  12828  xmulasslem  13181  ixxssixx  13256  iccshftri  13384  iccshftli  13386  iccdili  13388  icccntri  13390  elfz1b  13490  fzo1fzo0n0  13612  elfzonlteqm1  13638  elfzo0l  13653  ssfzo12  13656  fzoopth  13659  elfzo1elm1fzo0  13665  elfzr  13678  elfzlmr  13679  zmodidfzoimp  13802  mptnn0fsuppr  13903  seqp1  13920  seqcl2  13924  seqfveq2  13928  seqshft2  13932  monoord  13936  seqsplit  13939  seqcaopr3  13941  seqf1olem2a  13944  seqf1o  13947  seqid2  13952  seqhomo  13953  hashf1rn  14256  hashinfxadd  14289  hashf1lem2  14360  seqcoll  14368  hash2pr  14373  pr2pwpr  14383  hashge2el2difr  14385  hash3tr  14395  fi1uzind  14411  brfi1indALT  14414  elovmptnn0wrd  14463  swrdswrd  14609  pfxccatin12lem2a  14631  swrdccat  14639  swrdccatin1d  14647  swrdccatin2d  14648  repswccat  14690  cshwidxmod  14707  relexpsucnnr  14929  rtrclreclem3  14964  rtrclreclem4  14965  dfrtrcl2  14966  relexpindlem  14967  relexpind  14968  rtrclind  14969  cjre  15043  climeu  15459  climub  15566  fsum2d  15675  fsumabs  15705  fsumrlim  15715  fsumo1  15716  fsumiun  15725  prodfn0  15798  prodfrec  15799  ntrivcvg  15801  fprodabs  15878  fprod2d  15885  fprodefsum  15999  ruclem9  16144  dvdsmod0  16166  p1modz1  16167  dvdsmodexp  16168  dvdsabseq  16221  mod2eq1n2dvds  16255  mulsucdiv2z  16261  nno  16290  nn0o  16291  sadcadd  16366  sadadd2  16368  saddisjlem  16372  smuval2  16390  smupval  16396  smueqlem  16398  smumullem  16400  dfgcd2  16454  lcmgcdlem  16514  lcmftp  16544  exprmfct  16612  eulerthlem2  16690  dvdsprmpweqnn  16794  dvdsprmpweqle  16795  pcmpt  16801  vdwlem10  16899  cshwsidrepsw  17002  cshwshashlem1  17004  prmlem1a  17015  setsn0fun  17081  ressval3d  17154  mreexexd  17551  letsr  18496  insubm  18723  ghmghmrn  19145  pmtrfrn  19368  pmtr3ncom  19385  gsmtrcl  19426  psgnsn  19430  sylow1lem1  19508  efginvrel2  19637  efgsrel  19644  cntzcmnss  19751  gsum2dlem2  19881  telgsumfzs  19899  dprdval  19915  ablfac1eulem  19984  pgpfac1  19992  pgpfac  19996  srgpcomp  20134  ringrng  20201  ring1ne0  20215  rngimf1o  20370  rngimrnghm  20371  rngimcnv  20372  0ringnnzr  20438  zrhpsgnelbas  21529  psgndiflemA  21536  mplcoe1  21970  mplcoe3  21971  mplcoe5lem  21972  mplcoe5  21973  mpfaddcl  22038  mpfmulcl  22039  coe1ae0  22127  coe1fzgsumd  22217  gsummoncoe1  22221  pf1addcl  22266  pf1mulcl  22267  evl1gsumd  22270  mamufacex  22309  mat0dimcrng  22383  mavmulsolcl  22464  mdetunilem9  22533  cramerlem3  22602  pmatcollpw3fi1  22701  pm2mpfo  22727  chmaidscmat  22761  chfacfscmul0  22771  chfacfpmmul0  22775  cpmadugsumlemF  22789  tg2  22878  neindisj2  23036  neiptopnei  23045  t1t0  23261  fiuncmp  23317  hmeof1o  23677  ist1-5lem  23733  t1r0  23734  alexsublem  23957  imasdsf1olem  24286  tgioo  24709  fsumcn  24786  voliunlem3  25478  itgfsum  25753  dvbsss  25828  dvmptfsum  25904  dvfsumlem2  25958  dvfsumlem2OLD  25959  dvfsumlem4  25961  plyco  26171  dgrcolem1  26204  dgrco  26206  dvntaylp  26304  taylthlem1  26306  jensen  26924  bposlem5  27224  lgsqrmodndvds  27289  gausslemma2dlem0i  27300  gausslemma2dlem4  27305  lgsquad2lem2  27321  2lgslem3  27340  2lgs  27343  2lgsoddprm  27352  dchrisum0flb  27446  pntpbnd1  27522  pntlemf  27541  madebdayim  27831  oldbdayim  27832  pw2cut  28378  brbtwn  28875  brcgr  28876  umgrnloopv  29082  umgrnloop  29084  usgrnloopvALT  29177  usgrnloopALT  29179  usgredg2vlem2  29202  subgrprop  29249  uvtxnbgrvtx  29369  cusgrsize2inds  29430  rgrprop  29537  rusgrprop  29539  wlkprop  29588  wlkvtxeledg  29600  wlkeq  29610  wlkl1loop  29614  wlk1walk  29615  uspgr2wlkeqi  29624  wlkreslem  29644  wlkres  29645  redwlk  29647  lfgrwlknloop  29664  2pthnloop  29707  usgr2trlncl  29736  usgr2pth  29740  clwlkcompim  29756  clwlkcompbp  29758  uspgrn2crct  29784  crctcshwlkn0  29797  wwlknp  29819  wwlkswwlksn  29841  wlkiswwlks2lem4  29848  wlkiswwlks2  29851  wlklnwwlkln2lem  29858  wwlksnext  29869  wwlksnextbi  29870  wwlksnredwwlkn0  29872  wwlksnextwrd  29873  clwlkclwwlklem2a  29973  clwlkclwwlklem2  29975  clwlkclwwlkflem  29979  clwwisshclwws  29990  clwwlknp  30012  clwwlknwwlksn  30013  clwwlkwwlksb  30029  clwwlkext2edg  30031  umgrhashecclwwlk  30053  clwwlknun  30087  1pthond  30119  upgr3v3e3cycl  30155  upgr4cycl4dv4e  30160  eupth2  30214  3vfriswmgr  30253  3cyclfrgrrn1  30260  n4cyclfrgr  30266  frgrnbnb  30268  frgrncvvdeqlem3  30276  frgrncvvdeqlem6  30279  frgrncvvdeqlem7  30280  frgrncvvdeqlem8  30281  frgrwopreglem4a  30285  frgrwopreg  30298  frgrregorufr0  30299  frgr2wwlkeqm  30306  2clwwlk2clwwlklem  30321  wlkl0  30342  frgrreggt1  30368  frgrregord013  30370  frgrregord13  30371  frgrogt3nreg  30372  friendshipgt3  30373  friendship  30374  blocn2  30783  cvexchlem  32343  cdj3lem2b  32412  nnindf  32797  gsumwun  33040  domnprodn0  33237  issgon  34131  sitgclg  34350  sseqp1  34403  bnj938  34944  bnj964  34950  bnj1052  34982  bnj1125  34999  onvf1odlem4  35138  subfacp1lem6  35217  cvmliftlem7  35323  cvmliftlem10  35326  mclsrcl  35593  pprodss4v  35917  segleantisym  36148  rankeq1o  36204  bj-restv  37128  iooelexlt  37395  relowlssretop  37396  rdgeqoa  37403  matunitlindflem1  37655  poimirlem22  37681  poimirlem25  37684  poimirlem28  37687  poimirlem31  37690  mblfinlem3  37698  mbfresfi  37705  mettrifi  37796  opidon2OLD  37893  isexid2  37894  grpomndo  37914  elghomlem2OLD  37925  rngoidmlem  37975  rngoueqz  37979  iscringd  38037  cdlemk35s  40975  cdlemk39s  40977  cdlemk42  40979  uzindd  42009  mzpadd  42770  mzpmul  42771  mzpcompact2  42784  dford3lem2  43059  aomclem6  43091  cnsrexpcl  43197  ensucne0OLD  43562  pr2cv  43580  relexpss1d  43737  iunrelexpmin1  43740  iunrelexpmin2  43744  tfindsd  44242  nzin  44350  axc11next  44438  iotavalsb  44465  ssdec  45124  fperiodmullem  45343  monoordxrv  45518  fmul01  45619  fmulcl  45620  fmuldfeqlem1  45621  fmuldfeq  45622  iblspltprt  46010  itgspltprt  46016  stoweidlem2  46039  stoweidlem3  46040  stoweidlem6  46043  stoweidlem8  46045  stoweidlem17  46054  stoweidlem19  46056  stoweidlem21  46058  stoweidlem26  46063  stoweidlem31  46068  stoweidlem43  46080  fourierdlem42  46186  funressnfv  47073  eu2ndop1stv  47155  afv0fv0  47179  afv0nbfvbi  47181  funressnbrafv2  47274  funbrafv2  47277  nelbrim  47305  ssfz12  47344  smonoord  47401  iccpartiltu  47452  iccpartigtl  47453  iccelpart  47463  icceuelpart  47466  fargshiftf  47470  fargshiftf1  47471  fargshiftfo  47472  sprel  47514  sprsymrelf1lem  47521  sprsymrelfolem2  47523  prproropf1olem4  47536  lighneallem4  47640  mogoldbblem  47750  fpprnn  47760  fpprwppr  47769  fpprwpprb  47770  sbgoldbwt  47807  bgoldbtbndlem2  47836  bgoldbtbndlem4  47838  tgoldbach  47847  grimprop  47913  grlimprop  48014  grilcbri2  48041  upwlkwlk  48169  clcllaw  48221  intop  48233  clintop  48238  assintop  48239  assintopcllaw  48242  lmod0rng  48259  ztprmneprm  48377  scmsuppss  48401  ply1mulgsumlem1  48417  ply1mulgsumlem2  48418  lcoel0  48459  ellcoellss  48466  lindslinindsimp2lem5  48493  ldepspr  48504  flnn0div2ge  48564  nnolog2flm1  48621  blengt1fldiv2p1  48624  dignn0flhalf  48649  naryfvalelfv  48663  0aryfvalelfv  48666  fv1arycl  48668  fv2arycl  48679