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:  syldan  581  axc16i  2486  sbcn1  3686  sbcim1  3687  sbcbi1  3688  sbcel21v  3701  elimasni  5709  sotri  5741  unixpid  5891  f0rn0  6308  f1ocnv  6368  funbrfv  6457  f1dom3el3dif  6753  oprabid  6908  oprabv  6936  ndmovordi  7058  elovmpt2rab  7113  elovmpt2rab1  7114  elovmpt3rab1  7126  limomss  7303  unielxp  7439  bropfvvvvlem  7493  f1o2ndf1  7522  smogt  7703  tfrlem1  7711  oawordeulem  7874  omass  7900  ecopovtrn  8089  php  8386  unxpdom  8409  findcard2d  8444  findcard3  8445  isfinite2  8460  fsuppimp  8523  fsuppunfi  8537  fsuppunbi  8538  fsuppres  8542  cantnfval2  8816  cantnfle  8818  cantnfp1lem3  8827  cantnflem1  8836  cnfcom  8847  rankr1ai  8911  rankonidlem  8941  rankxplim2  8993  oncard  9072  ficardom  9073  cardne  9077  acnnum  9161  alephord2i  9186  cardaleph  9198  aceq3lem  9229  dfac5lem5  9236  dfac12lem3  9255  cdainf  9302  ackbij1lem16  9345  cfslb  9376  cfslb2n  9378  cfsmolem  9380  fin4i  9408  infpssr  9418  fin1a2lem6  9515  axdc3lem2  9561  axcclem  9567  ttukeylem6  9624  fodomb  9636  gchi  9734  fpwwe2lem5  9744  pwfseqlem4  9772  pwfseq  9774  inawina  9800  wunfi  9831  inar1  9885  ltexnq  10085  ltbtwnnq  10088  ltexprlem4  10149  ltexpri  10153  prlem936  10157  suplem1pr  10162  suplem2pr  10163  recexsrlem  10212  mulgt0sr  10214  map2psrpr  10219  supsr  10221  eqlei  10435  eqlei2  10436  ledivp1i  11237  nnind  11326  nnmulcl  11331  nnmulclOLD  11332  nn0ge2m1nn  11629  nnnegz  11649  ublbneg  11995  xmulasslem  12336  ixxssixx  12410  iccshftri  12533  iccshftli  12535  iccdili  12537  icccntri  12539  elfz1b  12635  fzo1fzo0n0  12746  elfzonlteqm1  12771  elfzo0l  12785  ssfzo12  12788  elfzo1elm1fzo0  12796  elfzr  12808  elfzlmr  12809  zmodidfzoimp  12927  mptnn0fsuppr  13025  seqp1  13042  seqcl2  13045  seqfveq2  13049  seqshft2  13053  monoord  13057  seqsplit  13060  seqcaopr3  13062  seqf1olem2a  13065  seqf1o  13068  seqid2  13073  seqhomo  13074  hashf1rn  13364  hashinfxadd  13395  hashf1lem2  13460  seqcoll  13468  hash2pr  13471  pr2pwpr  13481  hashge2el2difr  13483  hash3tr  13492  fi1uzind  13499  brfi1indALT  13502  elovmptnn0wrd  13563  swrdswrd  13687  swrdccatin12lem2a  13712  swrdccat  13720  swrdccatin1d  13726  swrdccatin2d  13727  swrdccatin12d  13728  repswccat  13759  cshwidxmod  13776  relexpsucnnr  13991  rtrclreclem3  14026  rtrclreclem4  14027  dfrtrcl2  14028  relexpindlem  14029  relexpind  14030  rtrclind  14031  cjre  14105  climeu  14512  climub  14618  fsum2d  14728  fsumabs  14758  fsumrlim  14768  fsumo1  14769  fsumiun  14778  prodfn0  14850  prodfrec  14851  ntrivcvg  14853  fprodabs  14928  fprod2d  14935  fprodefsum  15048  ruclem9  15190  dvdsmod0  15212  p1modz1  15213  dvdsmodexp  15214  dvdsabseq  15261  mod2eq1n2dvds  15294  mulsucdiv2z  15300  nno  15321  nn0o  15322  sadcadd  15402  sadadd2  15404  saddisjlem  15408  smuval2  15426  smupval  15432  smueqlem  15434  smumullem  15436  dfgcd2  15485  lcmgcdlem  15541  lcmftp  15571  exprmfct  15636  eulerthlem2  15707  dvdsprmpweqnn  15809  dvdsprmpweqle  15810  pcmpt  15816  vdwlem10  15914  cshwsidrepsw  16015  cshwshashlem1  16017  prmlem1a  16028  setsn0fun  16109  ressval3d  16151  ressval3dOLD  16152  mreexexd  16516  letsr  17435  ghmghmrn  17884  pmtrfrn  18082  pmtr3ncom  18099  gsmtrcl  18140  psgnsn  18144  sylow1lem1  18217  efginvrel2  18344  efgsrel  18351  cntzcmnss  18450  gsum2dlem2  18574  telgsumfzs  18591  dprdval  18607  ablfac1eulem  18676  pgpfac1  18684  pgpfac  18688  srgpcomp  18737  ring1ne0  18796  rimf1o  18941  rimrhm  18942  brric2  18952  0ringnnzr  19481  mplcoe1  19677  mplcoe3  19678  mplcoe5lem  19679  mplcoe5  19680  mpfaddcl  19745  mpfmulcl  19746  coe1ae0  19797  coe1fzgsumd  19883  gsummoncoe1  19885  pf1addcl  19928  pf1mulcl  19929  evl1gsumd  19932  zrhpsgnelbas  20151  psgndiflemA  20158  mamufacex  20409  mat0dimcrng  20491  mavmulsolcl  20572  mdetunilem9  20641  cramerlem3  20712  pmatcollpw3fi1  20810  pm2mpfo  20836  chmaidscmat  20870  chfacfscmul0  20880  chfacfpmmul0  20884  cpmadugsumlemF  20898  tg2  20987  neindisj2  21145  neiptopnei  21154  t1t0  21370  fiuncmp  21425  hmeof1o  21785  ist1-5lem  21841  t1r0  21842  alexsublem  22065  imasdsf1olem  22395  tgioo  22816  fsumcn  22890  voliunlem3  23539  itgfsum  23813  dvbsss  23886  dvmptfsum  23958  dvfsumlem2  24010  dvfsumlem4  24012  plyco  24217  dgrcolem1  24249  dgrco  24251  dvntaylp  24345  taylthlem1  24347  jensen  24935  bposlem5  25233  lgsqrmodndvds  25298  gausslemma2dlem0i  25309  gausslemma2dlem4  25314  lgsquad2lem2  25330  2lgslem3  25349  2lgs  25352  2lgsoddprm  25361  dchrisum0flb  25419  pntpbnd1  25495  pntlemf  25514  brbtwn  25999  brcgr  26000  umgrnloopv  26221  umgrnloop  26223  usgrnloopvALT  26314  usgrnloopALT  26316  usgredg2vlem2  26339  subgrprop  26387  uvtxnbgrvtx  26519  cusgrsize2inds  26583  rgrprop  26690  rusgrprop  26692  wlkprop  26741  wlkvtxeledg  26753  wlkeq  26763  wlkl1loop  26768  wlk1walk  26769  uspgr2wlkeqi  26778  wlkreslem  26800  wlkres  26801  redwlk  26803  lfgrwlknloop  26820  2pthnloop  26861  usgr2trlncl  26890  usgr2pth  26894  clwlkcompim  26910  clwlkcompbp  26912  uspgrn2crct  26935  crctcshwlkn0  26948  wwlknp  26970  wwlkswwlksn  26998  wlkiswwlks2lem4  27005  wlkiswwlks2  27008  wlklnwwlkln2lem  27015  wwlksnext  27036  wwlksnextbi  27037  wwlksnredwwlkn0  27039  wwlksnextwrd  27040  clwlkclwwlklem2a  27147  clwlkclwwlklem2  27149  clwlkclwwlkflem  27153  clwwisshclwws  27164  clwwlknp  27191  clwwlknwwlksn  27192  clwwlkwwlksb  27210  clwwlkext2edg  27212  umgrhashecclwwlk  27235  clwwlknun  27287  clwwlknunOLD  27292  1pthond  27323  upgr3v3e3cycl  27359  upgr4cycl4dv4e  27364  eupth2  27418  3vfriswmgr  27459  3cyclfrgrrn1  27466  n4cyclfrgr  27472  frgrnbnb  27474  frgrncvvdeqlem3  27482  frgrncvvdeqlem6  27485  frgrncvvdeqlem7  27486  frgrncvvdeqlem8  27487  frgrwopreglem4a  27491  frgrwopreg  27504  frgrregorufr0  27505  frgr2wwlkeqm  27512  2clwwlk2clwwlklem  27529  wlkl0  27553  frgrreggt1  27587  frgrregord013  27589  frgrregord13  27590  frgrogt3nreg  27591  friendshipgt3  27592  friendship  27593  blocn2  27997  cvexchlem  29561  cdj3lem2b  29630  cnvoprabOLD  29831  nnindf  29898  issgon  30517  sitgclg  30735  sseqp1  30788  bnj938  31335  bnj964  31341  bnj1052  31371  bnj1125  31388  subfacp1lem6  31495  cvmliftlem7  31601  cvmliftlem10  31604  mclsrcl  31786  pprodss4v  32317  segleantisym  32548  rankeq1o  32604  bj-restv  33361  iooelexlt  33528  relowlssretop  33529  rdgeqoa  33536  matunitlindflem1  33720  poimirlem22  33746  poimirlem25  33749  poimirlem28  33752  poimirlem31  33755  mblfinlem3  33763  mbfresfi  33770  mettrifi  33866  opidon2OLD  33966  isexid2  33967  grpomndo  33987  elghomlem2OLD  33998  rngoidmlem  34048  rngoueqz  34052  iscringd  34110  cdlemk35s  36719  cdlemk39s  36721  cdlemk42  36723  mzpadd  37804  mzpmul  37805  mzpcompact2  37818  dford3lem2  38096  aomclem6  38131  cnsrexpcl  38237  relexpss1d  38498  iunrelexpmin1  38501  iunrelexpmin2  38505  nzin  39018  axc11next  39107  iotavalsb  39134  ssdec  39759  fperiodmullem  39999  monoordxrv  40192  fmul01  40293  fmulcl  40294  fmuldfeqlem1  40295  fmuldfeq  40296  fprodcnlem  40312  iblspltprt  40669  itgspltprt  40675  stoweidlem2  40699  stoweidlem3  40700  stoweidlem6  40703  stoweidlem8  40705  stoweidlem17  40714  stoweidlem19  40716  stoweidlem21  40718  stoweidlem26  40723  stoweidlem31  40728  stoweidlem43  40740  fourierdlem42  40846  funressnfv  41663  eu2ndop1stv  41715  afv0fv0  41739  afv0nbfvbi  41741  funressnbrafv2  41834  funbrafv2  41837  nelbrim  41865  ssfz12  41900  fzoopth  41913  smonoord  41917  iccpartiltu  41934  iccpartigtl  41935  iccelpart  41945  icceuelpart  41948  fargshiftf  41952  fargshiftf1  41953  fargshiftfo  41954  lighneallem4  42103  mogoldbblem  42205  sbgoldbwt  42241  bgoldbtbndlem2  42270  bgoldbtbndlem4  42272  tgoldbach  42281  upwlkwlk  42289  sprel  42303  sprsymrelf1lem  42310  sprsymrelfolem2  42312  clcllaw  42396  intop  42408  clintop  42413  assintop  42414  assintopcllaw  42417  lmod0rng  42437  ringrng  42448  rngimf1o  42474  rngimrnghm  42475  ztprmneprm  42694  scmsuppss  42722  ply1mulgsumlem1  42743  ply1mulgsumlem2  42744  lcoel0  42786  ellcoellss  42793  lindslinindsimp2lem5  42820  ldepspr  42831  flnn0div2ge  42896  nnolog2flm1  42953  blengt1fldiv2p1  42956  dignn0flhalf  42981