Theorem mpcom 39

Description: Modus ponens inference with commutation of antecedents. Commuted form of mpd 16. (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 33	. 2 ⊢ (𝜓 → (𝜑 → 𝜒))
4	1, 3	mpd 16	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  681  axc16i  2470  mo4  2596  sbcn1  3799  sbcim1  3800  sbcbi1  3804  sbcel21v  3814  sbccomlem  3825  csbie2df  4400  elimasni  6084  sotri  6118  unixpid  6275  f0rn0  6753  f1ocnv  6823  funbrfv  6919  elfvmptrab1w  7007  f1dom3el3dif  7257  oprabidw  7431  oprabid  7432  oprabv  7460  ndmovordi  7591  elovmporab  7646  elovmporab1w  7647  elovmporab1  7648  elovmpt3rab1  7660  limomss  7855  unielxp  8012  bropfvvvvlem  8074  f1o2ndf1  8105  smogt  8342  tfrlem1  8350  oawordeulem  8527  omass  8553  ecopovtrn  8806  mapfvd  8865  findcard2d  9139  ssfi  9145  f1domfi  9153  php  9179  unxpdom  9207  findcard3  9231  isfinite2  9246  fsuppimp  9316  fsuppunfi  9336  fsuppunbi  9337  fsuppres  9341  infsupprpr  9454  cantnfval2  9626  cantnfle  9628  cantnfp1lem3  9637  cantnflem1  9646  cnfcom  9657  rankr1ai  9758  rankonidlem  9788  rankxplim2  9840  oncard  9934  ficardom  9935  cardne  9939  acnnum  10024  alephord2i  10049  cardaleph  10061  aceq3lem  10092  dfac5lem5  10099  dfac12lem3  10117  ackbij1lem16  10205  cfslb  10238  cfslb2n  10240  cfsmolem  10242  fin4i  10270  infpssr  10280  fin1a2lem6  10377  axdc3lem2  10423  axcclem  10429  ttukeylem6  10486  fodomb  10498  gchi  10597  pwfseq  10637  inawina  10663  wunfi  10694  inar1  10748  ltexnq  10948  ltbtwnnq  10951  ltexprlem4  11012  ltexpri  11016  prlem936  11020  suplem1pr  11025  suplem2pr  11026  recexsrlem  11076  mulgt0sr  11078  map2psrpr  11083  supsr  11085  eqlei  11308  eqlei2  11309  ledivp1i  12131  nnind  12242  nnmulcl  12248  nn0ge2m1nn  12565  nnnegz  12585  ublbneg  12948  xmulasslem  13302  ixxssixx  13377  iccshftri  13505  iccshftli  13507  iccdili  13509  icccntri  13511  elfz1b  13612  fzo1fzo0n0  13735  elfzonlteqm1  13761  elfzo0l  13776  ssfzo12  13779  fzoopth  13782  elfzo1elm1fzo0  13788  elfzr  13801  elfzlmr  13802  zmodidfzoimp  13925  mptnn0fsuppr  14026  seqp1  14043  seqcl2  14047  seqfveq2  14051  seqshft2  14055  monoord  14059  seqsplit  14062  seqcaopr3  14064  seqf1olem2a  14067  seqf1o  14070  seqid2  14075  seqhomo  14076  hashf1rn  14379  hashinfxadd  14412  hashf1lem2  14483  seqcoll  14491  hash2pr  14496  pr2pwpr  14506  hashge2el2difr  14508  hash3tr  14518  fi1uzind  14534  brfi1indALT  14537  elovmptnn0wrd  14586  swrdswrd  14732  pfxccatin12lem2a  14754  swrdccat  14762  swrdccatin1d  14770  swrdccatin2d  14771  repswccat  14813  cshwidxmod  14830  relexpsucnnr  15052  rtrclreclem3  15087  rtrclreclem4  15088  dfrtrcl2  15089  relexpindlem  15090  relexpind  15091  rtrclind  15092  cjre  15180  climeu  15596  climub  15703  fsum2d  15812  fsumabs  15843  fsumrlim  15853  fsumo1  15854  fsumiun  15863  prodfn0  15938  prodfrec  15939  ntrivcvg  15941  fprodabs  16018  fprod2d  16025  fprodefsum  16139  ruclem9  16284  dvdsmod0  16306  p1modz1  16307  dvdsmodexp  16308  dvdsabseq  16361  mod2eq1n2dvds  16395  mulsucdiv2z  16401  nno  16430  nn0o  16431  sadcadd  16506  sadadd2  16508  saddisjlem  16512  smuval2  16530  smupval  16536  smueqlem  16538  smumullem  16540  dfgcd2  16594  lcmgcdlem  16654  lcmftp  16684  exprmfct  16753  eulerthlem2  16831  dvdsprmpweqnn  16935  dvdsprmpweqle  16936  pcmpt  16942  vdwlem10  17040  cshwsidrepsw  17143  cshwshashlem1  17145  prmlem1a  17156  setsn0fun  17223  ressval3d  17296  mreexexd  17694  letsr  18639  insubm  18867  ghmghmrn  19296  pmtrfrn  19519  pmtr3ncom  19536  gsmtrcl  19577  psgnsn  19581  sylow1lem1  19659  efginvrel2  19788  efgsrel  19795  cntzcmnss  19902  gsum2dlem2  20032  telgsumfzs  20050  dprdval  20066  ablfac1eulem  20135  pgpfac1  20143  pgpfac  20147  srgpcomp  20291  ringrng  20359  ring1ne0  20373  rngimf1o  20527  rngimrnghm  20528  rngimcnv  20529  0ringnnzr  20600  zrhpsgnelbas  21704  psgndiflemA  21711  mplcoe1  22148  mplcoe3  22149  mplcoe5lem  22150  mplcoe5  22151  mpfaddcl  22224  mpfmulcl  22225  coe1ae0  22336  coe1fzgsumd  22425  gsummoncoe1  22429  pf1addcl  22474  pf1mulcl  22475  evl1gsumd  22478  mamufacex  22514  mat0dimcrng  22588  mavmulsolcl  22669  mdetunilem9  22738  cramerlem3  22807  pmatcollpw3fi1  22906  pm2mpfo  22932  chmaidscmat  22966  chfacfscmul0  22976  chfacfpmmul0  22980  cpmadugsumlemF  22994  tg2  23083  neindisj2  23241  neiptopnei  23250  t1t0  23466  fiuncmp  23522  hmeof1o  23882  ist1-5lem  23938  t1r0  23939  alexsublem  24162  imasdsf1olem  24491  tgioo  24914  fsumcn  24990  voliunlem3  25672  itgfsum  25947  dvbsss  26022  dvmptfsum  26095  dvfsumlem2  26147  dvfsumlem4  26149  plyco  26359  dgrcolem1  26391  dgrco  26393  dvntaylp  26492  taylthlem1  26494  jensen  27111  bposlem5  27410  lgsqrmodndvds  27475  gausslemma2dlem0i  27486  gausslemma2dlem4  27491  lgsquad2lem2  27507  2lgslem3  27526  2lgs  27529  2lgsoddprm  27538  dchrisum0flb  27632  pntpbnd1  27708  pntlemf  27727  madebdayim  28039  oldbdayim  28040  pw2cut  28611  brbtwn  29158  brcgr  29159  umgrnloopv  29365  umgrnloop  29367  usgrnloopvALT  29460  usgrnloopALT  29462  usgredg2vlem2  29485  subgrprop  29532  uvtxnbgrvtx  29652  cusgrsize2inds  29712  rgrprop  29819  rusgrprop  29821  wlkprop  29870  wlkvtxeledg  29882  wlkeq  29892  wlkl1loop  29896  wlk1walk  29897  uspgr2wlkeqi  29906  wlkreslem  29926  wlkres  29927  redwlk  29929  lfgrwlknloop  29946  2pthnloop  29989  usgr2trlncl  30018  usgr2pth  30022  clwlkcompim  30038  clwlkcompbp  30040  uspgrn2crct  30066  crctcshwlkn0  30079  wwlknp  30101  wwlkswwlksn  30123  wlkiswwlks2lem4  30130  wlkiswwlks2  30133  wlklnwwlkln2lem  30140  wwlksnext  30151  wwlksnextbi  30152  wwlksnredwwlkn0  30154  wwlksnextwrd  30155  clwlkclwwlklem2a  30258  clwlkclwwlklem2  30260  clwlkclwwlkflem  30264  clwwisshclwws  30275  clwwlknp  30297  clwwlknwwlksn  30298  clwwlkwwlksb  30314  clwwlkext2edg  30316  umgrhashecclwwlk  30338  clwwlknun  30372  1pthond  30404  upgr3v3e3cycl  30440  upgr4cycl4dv4e  30445  eupth2  30499  3vfriswmgr  30538  3cyclfrgrrn1  30545  n4cyclfrgr  30551  frgrnbnb  30553  frgrncvvdeqlem3  30561  frgrncvvdeqlem6  30564  frgrncvvdeqlem7  30565  frgrncvvdeqlem8  30566  frgrwopreglem4a  30570  frgrwopreg  30583  frgrregorufr0  30584  frgr2wwlkeqm  30591  2clwwlk2clwwlklem  30606  wlkl0  30627  frgrreggt1  30653  frgrregord013  30655  frgrregord13  30656  frgrogt3nreg  30657  friendshipgt3  30658  friendship  30659  blocn2  31069  cvexchlem  32629  cdj3lem2b  32698  nnindf  33077  gsumwun  33309  domnprodn0  33511  issgon  34430  sitgclg  34649  sseqp1  34702  bnj938  35242  bnj964  35248  bnj1052  35280  bnj1125  35297  onvf1odlem4  35461  subfacp1lem6  35548  cvmliftlem7  35654  cvmliftlem10  35657  mclsrcl  35924  pprodss4v  36245  segleantisym  36478  rankeq1o  36534  bj-restv  37597  iooelexlt  37868  relowlssretop  37869  rdgeqoa  37876  matunitlindflem1  38127  poimirlem22  38153  poimirlem25  38156  poimirlem28  38159  poimirlem31  38162  mblfinlem3  38170  mbfresfi  38177  mettrifi  38268  opidon2OLD  38365  isexid2  38366  grpomndo  38386  elghomlem2OLD  38397  rngoidmlem  38447  rngoueqz  38451  iscringd  38509  cdlemk35s  41573  cdlemk39s  41575  cdlemk42  41577  uzindd  42607  mzpadd  43331  mzpmul  43332  mzpcompact2  43345  dford3lem2  43616  aomclem6  43648  cnsrexpcl  43754  ensucne0OLD  44118  pr2cv  44136  relexpss1d  44293  iunrelexpmin1  44296  iunrelexpmin2  44300  tfindsd  44798  nzin  44892  axc11next  44980  iotavalsb  45007  ssdec  45664  fperiodmullem  45880  monoordxrv  46053  fmul01  46154  fmulcl  46155  fmuldfeqlem1  46156  fmuldfeq  46157  iblspltprt  46545  itgspltprt  46551  stoweidlem2  46574  stoweidlem3  46575  stoweidlem6  46578  stoweidlem8  46580  stoweidlem17  46589  stoweidlem19  46591  stoweidlem21  46593  stoweidlem26  46598  stoweidlem31  46603  stoweidlem43  46615  fourierdlem42  46721  funressnfv  47635  eu2ndop1stv  47717  afv0fv0  47741  afv0nbfvbi  47743  funressnbrafv2  47836  funbrafv2  47839  nelbrim  47867  ssfz12  47906  smonoord  47969  iccpartiltu  48026  iccpartigtl  48027  iccelpart  48037  icceuelpart  48040  fargshiftf  48044  fargshiftf1  48045  fargshiftfo  48046  sprel  48088  sprsymrelf1lem  48095  sprsymrelfolem2  48097  prproropf1olem4  48110  lighneallem4  48217  mogoldbblem  48340  fpprnn  48350  fpprwppr  48359  fpprwpprb  48360  sbgoldbwt  48397  bgoldbtbndlem2  48426  bgoldbtbndlem4  48428  tgoldbach  48437  grimprop  48503  grlimprop  48604  grilcbri2  48631  upwlkwlk  48759  clcllaw  48811  intop  48823  clintop  48828  assintop  48829  assintopcllaw  48832  lmod0rng  48849  ztprmneprm  48978  scmsuppss  49002  ply1mulgsumlem1  49017  ply1mulgsumlem2  49018  lcoel0  49059  ellcoellss  49066  lindslinindsimp2lem5  49093  ldepspr  49104  flnn0div2ge  49164  nnolog2flm1  49221  blengt1fldiv2p1  49224  dignn0flhalf  49249  naryfvalelfv  49263  0aryfvalelfv  49266  fv1arycl  49268  fv2arycl  49279