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  670  axc16i  2441  mo4  2567  sbcn1  3782  sbcim1  3783  sbcbi1  3787  sbcel21v  3797  sbccomlem  3808  csbie2df  4384  elimasni  6050  sotri  6084  unixpid  6242  f0rn0  6719  f1ocnv  6786  funbrfv  6882  elfvmptrab1w  6969  f1dom3el3dif  7217  oprabidw  7391  oprabid  7392  oprabv  7420  ndmovordi  7551  elovmporab  7606  elovmporab1w  7607  elovmporab1  7608  elovmpt3rab1  7620  limomss  7815  unielxp  7973  bropfvvvvlem  8034  f1o2ndf1  8065  smogt  8300  tfrlem1  8308  oawordeulem  8482  omass  8508  ecopovtrn  8760  mapfvd  8820  findcard2d  9094  ssfi  9100  f1domfi  9108  php  9134  unxpdom  9162  findcard3  9186  isfinite2  9201  fsuppimp  9274  fsuppunfi  9294  fsuppunbi  9295  fsuppres  9299  infsupprpr  9412  cantnfval2  9581  cantnfle  9583  cantnfp1lem3  9592  cantnflem1  9601  cnfcom  9612  rankr1ai  9713  rankonidlem  9743  rankxplim2  9795  oncard  9875  ficardom  9876  cardne  9880  acnnum  9965  alephord2i  9990  cardaleph  10002  aceq3lem  10033  dfac5lem5  10040  dfac12lem3  10059  ackbij1lem16  10147  cfslb  10179  cfslb2n  10181  cfsmolem  10183  fin4i  10211  infpssr  10221  fin1a2lem6  10318  axdc3lem2  10364  axcclem  10370  ttukeylem6  10427  fodomb  10439  gchi  10538  pwfseq  10578  inawina  10604  wunfi  10635  inar1  10689  ltexnq  10889  ltbtwnnq  10892  ltexprlem4  10953  ltexpri  10957  prlem936  10961  suplem1pr  10966  suplem2pr  10967  recexsrlem  11017  mulgt0sr  11019  map2psrpr  11024  supsr  11026  eqlei  11247  eqlei2  11248  ledivp1i  12072  nnind  12183  nnmulcl  12189  nn0ge2m1nn  12498  nnnegz  12518  ublbneg  12874  xmulasslem  13228  ixxssixx  13303  iccshftri  13431  iccshftli  13433  iccdili  13435  icccntri  13437  elfz1b  13538  fzo1fzo0n0  13661  elfzonlteqm1  13687  elfzo0l  13702  ssfzo12  13705  fzoopth  13708  elfzo1elm1fzo0  13714  elfzr  13727  elfzlmr  13728  zmodidfzoimp  13851  mptnn0fsuppr  13952  seqp1  13969  seqcl2  13973  seqfveq2  13977  seqshft2  13981  monoord  13985  seqsplit  13988  seqcaopr3  13990  seqf1olem2a  13993  seqf1o  13996  seqid2  14001  seqhomo  14002  hashf1rn  14305  hashinfxadd  14338  hashf1lem2  14409  seqcoll  14417  hash2pr  14422  pr2pwpr  14432  hashge2el2difr  14434  hash3tr  14444  fi1uzind  14460  brfi1indALT  14463  elovmptnn0wrd  14512  swrdswrd  14658  pfxccatin12lem2a  14680  swrdccat  14688  swrdccatin1d  14696  swrdccatin2d  14697  repswccat  14739  cshwidxmod  14756  relexpsucnnr  14978  rtrclreclem3  15013  rtrclreclem4  15014  dfrtrcl2  15015  relexpindlem  15016  relexpind  15017  rtrclind  15018  cjre  15092  climeu  15508  climub  15615  fsum2d  15724  fsumabs  15755  fsumrlim  15765  fsumo1  15766  fsumiun  15775  prodfn0  15850  prodfrec  15851  ntrivcvg  15853  fprodabs  15930  fprod2d  15937  fprodefsum  16051  ruclem9  16196  dvdsmod0  16218  p1modz1  16219  dvdsmodexp  16220  dvdsabseq  16273  mod2eq1n2dvds  16307  mulsucdiv2z  16313  nno  16342  nn0o  16343  sadcadd  16418  sadadd2  16420  saddisjlem  16424  smuval2  16442  smupval  16448  smueqlem  16450  smumullem  16452  dfgcd2  16506  lcmgcdlem  16566  lcmftp  16596  exprmfct  16665  eulerthlem2  16743  dvdsprmpweqnn  16847  dvdsprmpweqle  16848  pcmpt  16854  vdwlem10  16952  cshwsidrepsw  17055  cshwshashlem1  17057  prmlem1a  17068  setsn0fun  17134  ressval3d  17207  mreexexd  17605  letsr  18550  insubm  18777  ghmghmrn  19201  pmtrfrn  19424  pmtr3ncom  19441  gsmtrcl  19482  psgnsn  19486  sylow1lem1  19564  efginvrel2  19693  efgsrel  19700  cntzcmnss  19807  gsum2dlem2  19937  telgsumfzs  19955  dprdval  19971  ablfac1eulem  20040  pgpfac1  20048  pgpfac  20052  srgpcomp  20190  ringrng  20257  ring1ne0  20271  rngimf1o  20425  rngimrnghm  20426  rngimcnv  20427  0ringnnzr  20493  zrhpsgnelbas  21584  psgndiflemA  21591  mplcoe1  22025  mplcoe3  22026  mplcoe5lem  22027  mplcoe5  22028  mpfaddcl  22101  mpfmulcl  22102  coe1ae0  22190  coe1fzgsumd  22279  gsummoncoe1  22283  pf1addcl  22328  pf1mulcl  22329  evl1gsumd  22332  mamufacex  22371  mat0dimcrng  22445  mavmulsolcl  22526  mdetunilem9  22595  cramerlem3  22664  pmatcollpw3fi1  22763  pm2mpfo  22789  chmaidscmat  22823  chfacfscmul0  22833  chfacfpmmul0  22837  cpmadugsumlemF  22851  tg2  22940  neindisj2  23098  neiptopnei  23107  t1t0  23323  fiuncmp  23379  hmeof1o  23739  ist1-5lem  23795  t1r0  23796  alexsublem  24019  imasdsf1olem  24348  tgioo  24771  fsumcn  24847  voliunlem3  25529  itgfsum  25804  dvbsss  25879  dvmptfsum  25952  dvfsumlem2  26004  dvfsumlem4  26006  plyco  26216  dgrcolem1  26248  dgrco  26250  dvntaylp  26348  taylthlem1  26350  jensen  26966  bposlem5  27265  lgsqrmodndvds  27330  gausslemma2dlem0i  27341  gausslemma2dlem4  27346  lgsquad2lem2  27362  2lgslem3  27381  2lgs  27384  2lgsoddprm  27393  dchrisum0flb  27487  pntpbnd1  27563  pntlemf  27582  madebdayim  27894  oldbdayim  27895  pw2cut  28466  brbtwn  28982  brcgr  28983  umgrnloopv  29189  umgrnloop  29191  usgrnloopvALT  29284  usgrnloopALT  29286  usgredg2vlem2  29309  subgrprop  29356  uvtxnbgrvtx  29476  cusgrsize2inds  29537  rgrprop  29644  rusgrprop  29646  wlkprop  29695  wlkvtxeledg  29707  wlkeq  29717  wlkl1loop  29721  wlk1walk  29722  uspgr2wlkeqi  29731  wlkreslem  29751  wlkres  29752  redwlk  29754  lfgrwlknloop  29771  2pthnloop  29814  usgr2trlncl  29843  usgr2pth  29847  clwlkcompim  29863  clwlkcompbp  29865  uspgrn2crct  29891  crctcshwlkn0  29904  wwlknp  29926  wwlkswwlksn  29948  wlkiswwlks2lem4  29955  wlkiswwlks2  29958  wlklnwwlkln2lem  29965  wwlksnext  29976  wwlksnextbi  29977  wwlksnredwwlkn0  29979  wwlksnextwrd  29980  clwlkclwwlklem2a  30083  clwlkclwwlklem2  30085  clwlkclwwlkflem  30089  clwwisshclwws  30100  clwwlknp  30122  clwwlknwwlksn  30123  clwwlkwwlksb  30139  clwwlkext2edg  30141  umgrhashecclwwlk  30163  clwwlknun  30197  1pthond  30229  upgr3v3e3cycl  30265  upgr4cycl4dv4e  30270  eupth2  30324  3vfriswmgr  30363  3cyclfrgrrn1  30370  n4cyclfrgr  30376  frgrnbnb  30378  frgrncvvdeqlem3  30386  frgrncvvdeqlem6  30389  frgrncvvdeqlem7  30390  frgrncvvdeqlem8  30391  frgrwopreglem4a  30395  frgrwopreg  30408  frgrregorufr0  30409  frgr2wwlkeqm  30416  2clwwlk2clwwlklem  30431  wlkl0  30452  frgrreggt1  30478  frgrregord013  30480  frgrregord13  30481  frgrogt3nreg  30482  friendshipgt3  30483  friendship  30484  blocn2  30894  cvexchlem  32454  cdj3lem2b  32523  nnindf  32908  gsumwun  33152  domnprodn0  33351  issgon  34283  sitgclg  34502  sseqp1  34555  bnj938  35095  bnj964  35101  bnj1052  35133  bnj1125  35150  onvf1odlem4  35304  subfacp1lem6  35383  cvmliftlem7  35489  cvmliftlem10  35492  mclsrcl  35759  pprodss4v  36080  segleantisym  36313  rankeq1o  36369  bj-restv  37423  iooelexlt  37692  relowlssretop  37693  rdgeqoa  37700  matunitlindflem1  37951  poimirlem22  37977  poimirlem25  37980  poimirlem28  37983  poimirlem31  37986  mblfinlem3  37994  mbfresfi  38001  mettrifi  38092  opidon2OLD  38189  isexid2  38190  grpomndo  38210  elghomlem2OLD  38221  rngoidmlem  38271  rngoueqz  38275  iscringd  38333  cdlemk35s  41397  cdlemk39s  41399  cdlemk42  41401  uzindd  42431  mzpadd  43184  mzpmul  43185  mzpcompact2  43198  dford3lem2  43473  aomclem6  43505  cnsrexpcl  43611  ensucne0OLD  43975  pr2cv  43993  relexpss1d  44150  iunrelexpmin1  44153  iunrelexpmin2  44157  tfindsd  44655  nzin  44763  axc11next  44851  iotavalsb  44878  ssdec  45536  fperiodmullem  45754  monoordxrv  45927  fmul01  46028  fmulcl  46029  fmuldfeqlem1  46030  fmuldfeq  46031  iblspltprt  46419  itgspltprt  46425  stoweidlem2  46448  stoweidlem3  46449  stoweidlem6  46452  stoweidlem8  46454  stoweidlem17  46463  stoweidlem19  46465  stoweidlem21  46467  stoweidlem26  46472  stoweidlem31  46477  stoweidlem43  46489  fourierdlem42  46595  funressnfv  47503  eu2ndop1stv  47585  afv0fv0  47609  afv0nbfvbi  47611  funressnbrafv2  47704  funbrafv2  47707  nelbrim  47735  ssfz12  47774  smonoord  47837  iccpartiltu  47894  iccpartigtl  47895  iccelpart  47905  icceuelpart  47908  fargshiftf  47912  fargshiftf1  47913  fargshiftfo  47914  sprel  47956  sprsymrelf1lem  47963  sprsymrelfolem2  47965  prproropf1olem4  47978  lighneallem4  48085  mogoldbblem  48208  fpprnn  48218  fpprwppr  48227  fpprwpprb  48228  sbgoldbwt  48265  bgoldbtbndlem2  48294  bgoldbtbndlem4  48296  tgoldbach  48305  grimprop  48371  grlimprop  48472  grilcbri2  48499  upwlkwlk  48627  clcllaw  48679  intop  48691  clintop  48696  assintop  48697  assintopcllaw  48700  lmod0rng  48717  ztprmneprm  48835  scmsuppss  48859  ply1mulgsumlem1  48874  ply1mulgsumlem2  48875  lcoel0  48916  ellcoellss  48923  lindslinindsimp2lem5  48950  ldepspr  48961  flnn0div2ge  49021  nnolog2flm1  49078  blengt1fldiv2p1  49081  dignn0flhalf  49106  naryfvalelfv  49120  0aryfvalelfv  49123  fv1arycl  49125  fv2arycl  49136