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  2434  mo4  2559  sbcn1  3806  sbcim1  3807  sbcbi1  3811  sbcel21v  3821  sbccomlem  3832  csbie2df  4406  elimasni  6062  sotri  6100  unixpid  6257  f0rn0  6745  f1ocnv  6812  funbrfv  6909  elfvmptrab1w  6995  f1dom3el3dif  7244  oprabidw  7418  oprabid  7419  oprabv  7449  ndmovordi  7580  elovmporab  7635  elovmporab1w  7636  elovmporab1  7637  elovmpt3rab1  7649  limomss  7847  unielxp  8006  bropfvvvvlem  8070  f1o2ndf1  8101  smogt  8336  tfrlem1  8344  oawordeulem  8518  omass  8544  ecopovtrn  8793  mapfvd  8852  findcard2d  9130  ssfi  9137  f1domfi  9145  php  9171  unxpdom  9200  findcard3  9229  findcard3OLD  9230  isfinite2  9245  fsuppimp  9319  fsuppunfi  9339  fsuppunbi  9340  fsuppres  9344  infsupprpr  9457  cantnfval2  9622  cantnfle  9624  cantnfp1lem3  9633  cantnflem1  9642  cnfcom  9653  rankr1ai  9751  rankonidlem  9781  rankxplim2  9833  oncard  9913  ficardom  9914  cardne  9918  acnnum  10005  alephord2i  10030  cardaleph  10042  aceq3lem  10073  dfac5lem5  10080  dfac12lem3  10099  ackbij1lem16  10187  cfslb  10219  cfslb2n  10221  cfsmolem  10223  fin4i  10251  infpssr  10261  fin1a2lem6  10358  axdc3lem2  10404  axcclem  10410  ttukeylem6  10467  fodomb  10479  gchi  10577  pwfseq  10617  inawina  10643  wunfi  10674  inar1  10728  ltexnq  10928  ltbtwnnq  10931  ltexprlem4  10992  ltexpri  10996  prlem936  11000  suplem1pr  11005  suplem2pr  11006  recexsrlem  11056  mulgt0sr  11058  map2psrpr  11063  supsr  11065  eqlei  11284  eqlei2  11285  ledivp1i  12108  nnind  12204  nnmulcl  12210  nn0ge2m1nn  12512  nnnegz  12532  ublbneg  12892  xmulasslem  13245  ixxssixx  13320  iccshftri  13448  iccshftli  13450  iccdili  13452  icccntri  13454  elfz1b  13554  fzo1fzo0n0  13676  elfzonlteqm1  13702  elfzo0l  13717  ssfzo12  13720  fzoopth  13723  elfzo1elm1fzo0  13729  elfzr  13741  elfzlmr  13742  zmodidfzoimp  13863  mptnn0fsuppr  13964  seqp1  13981  seqcl2  13985  seqfveq2  13989  seqshft2  13993  monoord  13997  seqsplit  14000  seqcaopr3  14002  seqf1olem2a  14005  seqf1o  14008  seqid2  14013  seqhomo  14014  hashf1rn  14317  hashinfxadd  14350  hashf1lem2  14421  seqcoll  14429  hash2pr  14434  pr2pwpr  14444  hashge2el2difr  14446  hash3tr  14456  fi1uzind  14472  brfi1indALT  14475  elovmptnn0wrd  14524  swrdswrd  14670  pfxccatin12lem2a  14692  swrdccat  14700  swrdccatin1d  14708  swrdccatin2d  14709  repswccat  14751  cshwidxmod  14768  relexpsucnnr  14991  rtrclreclem3  15026  rtrclreclem4  15027  dfrtrcl2  15028  relexpindlem  15029  relexpind  15030  rtrclind  15031  cjre  15105  climeu  15521  climub  15628  fsum2d  15737  fsumabs  15767  fsumrlim  15777  fsumo1  15778  fsumiun  15787  prodfn0  15860  prodfrec  15861  ntrivcvg  15863  fprodabs  15940  fprod2d  15947  fprodefsum  16061  ruclem9  16206  dvdsmod0  16228  p1modz1  16229  dvdsmodexp  16230  dvdsabseq  16283  mod2eq1n2dvds  16317  mulsucdiv2z  16323  nno  16352  nn0o  16353  sadcadd  16428  sadadd2  16430  saddisjlem  16434  smuval2  16452  smupval  16458  smueqlem  16460  smumullem  16462  dfgcd2  16516  lcmgcdlem  16576  lcmftp  16606  exprmfct  16674  eulerthlem2  16752  dvdsprmpweqnn  16856  dvdsprmpweqle  16857  pcmpt  16863  vdwlem10  16961  cshwsidrepsw  17064  cshwshashlem1  17066  prmlem1a  17077  setsn0fun  17143  ressval3d  17216  mreexexd  17609  letsr  18552  insubm  18745  ghmghmrn  19167  pmtrfrn  19388  pmtr3ncom  19405  gsmtrcl  19446  psgnsn  19450  sylow1lem1  19528  efginvrel2  19657  efgsrel  19664  cntzcmnss  19771  gsum2dlem2  19901  telgsumfzs  19919  dprdval  19935  ablfac1eulem  20004  pgpfac1  20012  pgpfac  20016  srgpcomp  20127  ringrng  20194  ring1ne0  20208  rngimf1o  20363  rngimrnghm  20364  rngimcnv  20365  0ringnnzr  20434  zrhpsgnelbas  21503  psgndiflemA  21510  mplcoe1  21944  mplcoe3  21945  mplcoe5lem  21946  mplcoe5  21947  mpfaddcl  22012  mpfmulcl  22013  coe1ae0  22101  coe1fzgsumd  22191  gsummoncoe1  22195  pf1addcl  22240  pf1mulcl  22241  evl1gsumd  22244  mamufacex  22283  mat0dimcrng  22357  mavmulsolcl  22438  mdetunilem9  22507  cramerlem3  22576  pmatcollpw3fi1  22675  pm2mpfo  22701  chmaidscmat  22735  chfacfscmul0  22745  chfacfpmmul0  22749  cpmadugsumlemF  22763  tg2  22852  neindisj2  23010  neiptopnei  23019  t1t0  23235  fiuncmp  23291  hmeof1o  23651  ist1-5lem  23707  t1r0  23708  alexsublem  23931  imasdsf1olem  24261  tgioo  24684  fsumcn  24761  voliunlem3  25453  itgfsum  25728  dvbsss  25803  dvmptfsum  25879  dvfsumlem2  25933  dvfsumlem2OLD  25934  dvfsumlem4  25936  plyco  26146  dgrcolem1  26179  dgrco  26181  dvntaylp  26279  taylthlem1  26281  jensen  26899  bposlem5  27199  lgsqrmodndvds  27264  gausslemma2dlem0i  27275  gausslemma2dlem4  27280  lgsquad2lem2  27296  2lgslem3  27315  2lgs  27318  2lgsoddprm  27327  dchrisum0flb  27421  pntpbnd1  27497  pntlemf  27516  madebdayim  27799  oldbdayim  27800  pw2cut  28335  brbtwn  28826  brcgr  28827  umgrnloopv  29033  umgrnloop  29035  usgrnloopvALT  29128  usgrnloopALT  29130  usgredg2vlem2  29153  subgrprop  29200  uvtxnbgrvtx  29320  cusgrsize2inds  29381  rgrprop  29488  rusgrprop  29490  wlkprop  29539  wlkvtxeledg  29552  wlkeq  29562  wlkl1loop  29566  wlk1walk  29567  uspgr2wlkeqi  29576  wlkreslem  29597  wlkres  29598  redwlk  29600  lfgrwlknloop  29617  2pthnloop  29661  usgr2trlncl  29690  usgr2pth  29694  clwlkcompim  29710  clwlkcompbp  29712  uspgrn2crct  29738  crctcshwlkn0  29751  wwlknp  29773  wwlkswwlksn  29795  wlkiswwlks2lem4  29802  wlkiswwlks2  29805  wlklnwwlkln2lem  29812  wwlksnext  29823  wwlksnextbi  29824  wwlksnredwwlkn0  29826  wwlksnextwrd  29827  clwlkclwwlklem2a  29927  clwlkclwwlklem2  29929  clwlkclwwlkflem  29933  clwwisshclwws  29944  clwwlknp  29966  clwwlknwwlksn  29967  clwwlkwwlksb  29983  clwwlkext2edg  29985  umgrhashecclwwlk  30007  clwwlknun  30041  1pthond  30073  upgr3v3e3cycl  30109  upgr4cycl4dv4e  30114  eupth2  30168  3vfriswmgr  30207  3cyclfrgrrn1  30214  n4cyclfrgr  30220  frgrnbnb  30222  frgrncvvdeqlem3  30230  frgrncvvdeqlem6  30233  frgrncvvdeqlem7  30234  frgrncvvdeqlem8  30235  frgrwopreglem4a  30239  frgrwopreg  30252  frgrregorufr0  30253  frgr2wwlkeqm  30260  2clwwlk2clwwlklem  30275  wlkl0  30296  frgrreggt1  30322  frgrregord013  30324  frgrregord13  30325  frgrogt3nreg  30326  friendshipgt3  30327  friendship  30328  blocn2  30737  cvexchlem  32297  cdj3lem2b  32366  nnindf  32744  gsumwun  33005  domnprodn0  33226  issgon  34113  sitgclg  34333  sseqp1  34386  bnj938  34927  bnj964  34933  bnj1052  34965  bnj1125  34982  onvf1odlem4  35093  subfacp1lem6  35172  cvmliftlem7  35278  cvmliftlem10  35281  mclsrcl  35548  pprodss4v  35872  segleantisym  36103  rankeq1o  36159  bj-restv  37083  iooelexlt  37350  relowlssretop  37351  rdgeqoa  37358  matunitlindflem1  37610  poimirlem22  37636  poimirlem25  37639  poimirlem28  37642  poimirlem31  37645  mblfinlem3  37653  mbfresfi  37660  mettrifi  37751  opidon2OLD  37848  isexid2  37849  grpomndo  37869  elghomlem2OLD  37880  rngoidmlem  37930  rngoueqz  37934  iscringd  37992  cdlemk35s  40931  cdlemk39s  40933  cdlemk42  40935  uzindd  41965  mzpadd  42726  mzpmul  42727  mzpcompact2  42740  dford3lem2  43016  aomclem6  43048  cnsrexpcl  43154  ensucne0OLD  43519  pr2cv  43537  relexpss1d  43694  iunrelexpmin1  43697  iunrelexpmin2  43701  tfindsd  44199  nzin  44307  axc11next  44395  iotavalsb  44422  ssdec  45082  fperiodmullem  45301  monoordxrv  45477  fmul01  45578  fmulcl  45579  fmuldfeqlem1  45580  fmuldfeq  45581  iblspltprt  45971  itgspltprt  45977  stoweidlem2  46000  stoweidlem3  46001  stoweidlem6  46004  stoweidlem8  46006  stoweidlem17  46015  stoweidlem19  46017  stoweidlem21  46019  stoweidlem26  46024  stoweidlem31  46029  stoweidlem43  46041  fourierdlem42  46147  funressnfv  47044  eu2ndop1stv  47126  afv0fv0  47150  afv0nbfvbi  47152  funressnbrafv2  47245  funbrafv2  47248  nelbrim  47276  ssfz12  47315  smonoord  47372  iccpartiltu  47423  iccpartigtl  47424  iccelpart  47434  icceuelpart  47437  fargshiftf  47441  fargshiftf1  47442  fargshiftfo  47443  sprel  47485  sprsymrelf1lem  47492  sprsymrelfolem2  47494  prproropf1olem4  47507  lighneallem4  47611  mogoldbblem  47721  fpprnn  47731  fpprwppr  47740  fpprwpprb  47741  sbgoldbwt  47778  bgoldbtbndlem2  47807  bgoldbtbndlem4  47809  tgoldbach  47818  grimprop  47883  grlimprop  47983  grilcbri2  48003  upwlkwlk  48127  clcllaw  48179  intop  48191  clintop  48196  assintop  48197  assintopcllaw  48200  lmod0rng  48217  ztprmneprm  48335  scmsuppss  48359  ply1mulgsumlem1  48375  ply1mulgsumlem2  48376  lcoel0  48417  ellcoellss  48424  lindslinindsimp2lem5  48451  ldepspr  48462  flnn0div2ge  48522  nnolog2flm1  48579  blengt1fldiv2p1  48582  dignn0flhalf  48607  naryfvalelfv  48621  0aryfvalelfv  48624  fv1arycl  48626  fv2arycl  48637