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  2438  mo4  2563  sbcn1  3790  sbcim1  3791  sbcbi1  3795  sbcel21v  3805  sbccomlem  3816  csbie2df  4392  elimasni  6044  sotri  6078  unixpid  6236  f0rn0  6713  f1ocnv  6780  funbrfv  6876  elfvmptrab1w  6962  f1dom3el3dif  7209  oprabidw  7383  oprabid  7384  oprabv  7412  ndmovordi  7543  elovmporab  7598  elovmporab1w  7599  elovmporab1  7600  elovmpt3rab1  7612  limomss  7807  unielxp  7965  bropfvvvvlem  8027  f1o2ndf1  8058  smogt  8293  tfrlem1  8301  oawordeulem  8475  omass  8501  ecopovtrn  8750  mapfvd  8809  findcard2d  9083  ssfi  9089  f1domfi  9097  php  9123  unxpdom  9150  findcard3  9174  isfinite2  9189  fsuppimp  9259  fsuppunfi  9279  fsuppunbi  9280  fsuppres  9284  infsupprpr  9397  cantnfval2  9566  cantnfle  9568  cantnfp1lem3  9577  cantnflem1  9586  cnfcom  9597  rankr1ai  9698  rankonidlem  9728  rankxplim2  9780  oncard  9860  ficardom  9861  cardne  9865  acnnum  9950  alephord2i  9975  cardaleph  9987  aceq3lem  10018  dfac5lem5  10025  dfac12lem3  10044  ackbij1lem16  10132  cfslb  10164  cfslb2n  10166  cfsmolem  10168  fin4i  10196  infpssr  10206  fin1a2lem6  10303  axdc3lem2  10349  axcclem  10355  ttukeylem6  10412  fodomb  10424  gchi  10522  pwfseq  10562  inawina  10588  wunfi  10619  inar1  10673  ltexnq  10873  ltbtwnnq  10876  ltexprlem4  10937  ltexpri  10941  prlem936  10945  suplem1pr  10950  suplem2pr  10951  recexsrlem  11001  mulgt0sr  11003  map2psrpr  11008  supsr  11010  eqlei  11230  eqlei2  11231  ledivp1i  12054  nnind  12150  nnmulcl  12156  nn0ge2m1nn  12458  nnnegz  12478  ublbneg  12833  xmulasslem  13186  ixxssixx  13261  iccshftri  13389  iccshftli  13391  iccdili  13393  icccntri  13395  elfz1b  13495  fzo1fzo0n0  13617  elfzonlteqm1  13643  elfzo0l  13658  ssfzo12  13661  fzoopth  13664  elfzo1elm1fzo0  13670  elfzr  13683  elfzlmr  13684  zmodidfzoimp  13807  mptnn0fsuppr  13908  seqp1  13925  seqcl2  13929  seqfveq2  13933  seqshft2  13937  monoord  13941  seqsplit  13944  seqcaopr3  13946  seqf1olem2a  13949  seqf1o  13952  seqid2  13957  seqhomo  13958  hashf1rn  14261  hashinfxadd  14294  hashf1lem2  14365  seqcoll  14373  hash2pr  14378  pr2pwpr  14388  hashge2el2difr  14390  hash3tr  14400  fi1uzind  14416  brfi1indALT  14419  elovmptnn0wrd  14468  swrdswrd  14614  pfxccatin12lem2a  14636  swrdccat  14644  swrdccatin1d  14652  swrdccatin2d  14653  repswccat  14695  cshwidxmod  14712  relexpsucnnr  14934  rtrclreclem3  14969  rtrclreclem4  14970  dfrtrcl2  14971  relexpindlem  14972  relexpind  14973  rtrclind  14974  cjre  15048  climeu  15464  climub  15571  fsum2d  15680  fsumabs  15710  fsumrlim  15720  fsumo1  15721  fsumiun  15730  prodfn0  15803  prodfrec  15804  ntrivcvg  15806  fprodabs  15883  fprod2d  15890  fprodefsum  16004  ruclem9  16149  dvdsmod0  16171  p1modz1  16172  dvdsmodexp  16173  dvdsabseq  16226  mod2eq1n2dvds  16260  mulsucdiv2z  16266  nno  16295  nn0o  16296  sadcadd  16371  sadadd2  16373  saddisjlem  16377  smuval2  16395  smupval  16401  smueqlem  16403  smumullem  16405  dfgcd2  16459  lcmgcdlem  16519  lcmftp  16549  exprmfct  16617  eulerthlem2  16695  dvdsprmpweqnn  16799  dvdsprmpweqle  16800  pcmpt  16806  vdwlem10  16904  cshwsidrepsw  17007  cshwshashlem1  17009  prmlem1a  17020  setsn0fun  17086  ressval3d  17159  mreexexd  17556  letsr  18501  insubm  18728  ghmghmrn  19149  pmtrfrn  19372  pmtr3ncom  19389  gsmtrcl  19430  psgnsn  19434  sylow1lem1  19512  efginvrel2  19641  efgsrel  19648  cntzcmnss  19755  gsum2dlem2  19885  telgsumfzs  19903  dprdval  19919  ablfac1eulem  19988  pgpfac1  19996  pgpfac  20000  srgpcomp  20138  ringrng  20205  ring1ne0  20219  rngimf1o  20374  rngimrnghm  20375  rngimcnv  20376  0ringnnzr  20442  zrhpsgnelbas  21533  psgndiflemA  21540  mplcoe1  21973  mplcoe3  21974  mplcoe5lem  21975  mplcoe5  21976  mpfaddcl  22041  mpfmulcl  22042  coe1ae0  22130  coe1fzgsumd  22220  gsummoncoe1  22224  pf1addcl  22269  pf1mulcl  22270  evl1gsumd  22273  mamufacex  22312  mat0dimcrng  22386  mavmulsolcl  22467  mdetunilem9  22536  cramerlem3  22605  pmatcollpw3fi1  22704  pm2mpfo  22730  chmaidscmat  22764  chfacfscmul0  22774  chfacfpmmul0  22778  cpmadugsumlemF  22792  tg2  22881  neindisj2  23039  neiptopnei  23048  t1t0  23264  fiuncmp  23320  hmeof1o  23680  ist1-5lem  23736  t1r0  23737  alexsublem  23960  imasdsf1olem  24289  tgioo  24712  fsumcn  24789  voliunlem3  25481  itgfsum  25756  dvbsss  25831  dvmptfsum  25907  dvfsumlem2  25961  dvfsumlem2OLD  25962  dvfsumlem4  25964  plyco  26174  dgrcolem1  26207  dgrco  26209  dvntaylp  26307  taylthlem1  26309  jensen  26927  bposlem5  27227  lgsqrmodndvds  27292  gausslemma2dlem0i  27303  gausslemma2dlem4  27308  lgsquad2lem2  27324  2lgslem3  27343  2lgs  27346  2lgsoddprm  27355  dchrisum0flb  27449  pntpbnd1  27525  pntlemf  27544  madebdayim  27834  oldbdayim  27835  pw2cut  28381  brbtwn  28879  brcgr  28880  umgrnloopv  29086  umgrnloop  29088  usgrnloopvALT  29181  usgrnloopALT  29183  usgredg2vlem2  29206  subgrprop  29253  uvtxnbgrvtx  29373  cusgrsize2inds  29434  rgrprop  29541  rusgrprop  29543  wlkprop  29592  wlkvtxeledg  29604  wlkeq  29614  wlkl1loop  29618  wlk1walk  29619  uspgr2wlkeqi  29628  wlkreslem  29648  wlkres  29649  redwlk  29651  lfgrwlknloop  29668  2pthnloop  29711  usgr2trlncl  29740  usgr2pth  29744  clwlkcompim  29760  clwlkcompbp  29762  uspgrn2crct  29788  crctcshwlkn0  29801  wwlknp  29823  wwlkswwlksn  29845  wlkiswwlks2lem4  29852  wlkiswwlks2  29855  wlklnwwlkln2lem  29862  wwlksnext  29873  wwlksnextbi  29874  wwlksnredwwlkn0  29876  wwlksnextwrd  29877  clwlkclwwlklem2a  29980  clwlkclwwlklem2  29982  clwlkclwwlkflem  29986  clwwisshclwws  29997  clwwlknp  30019  clwwlknwwlksn  30020  clwwlkwwlksb  30036  clwwlkext2edg  30038  umgrhashecclwwlk  30060  clwwlknun  30094  1pthond  30126  upgr3v3e3cycl  30162  upgr4cycl4dv4e  30167  eupth2  30221  3vfriswmgr  30260  3cyclfrgrrn1  30267  n4cyclfrgr  30273  frgrnbnb  30275  frgrncvvdeqlem3  30283  frgrncvvdeqlem6  30286  frgrncvvdeqlem7  30287  frgrncvvdeqlem8  30288  frgrwopreglem4a  30292  frgrwopreg  30305  frgrregorufr0  30306  frgr2wwlkeqm  30313  2clwwlk2clwwlklem  30328  wlkl0  30349  frgrreggt1  30375  frgrregord013  30377  frgrregord13  30378  frgrogt3nreg  30379  friendshipgt3  30380  friendship  30381  blocn2  30790  cvexchlem  32350  cdj3lem2b  32419  nnindf  32807  gsumwun  33052  domnprodn0  33249  issgon  34157  sitgclg  34376  sseqp1  34429  bnj938  34970  bnj964  34976  bnj1052  35008  bnj1125  35025  onvf1odlem4  35171  subfacp1lem6  35250  cvmliftlem7  35356  cvmliftlem10  35359  mclsrcl  35626  pprodss4v  35947  segleantisym  36180  rankeq1o  36236  bj-restv  37160  iooelexlt  37427  relowlssretop  37428  rdgeqoa  37435  matunitlindflem1  37676  poimirlem22  37702  poimirlem25  37705  poimirlem28  37708  poimirlem31  37711  mblfinlem3  37719  mbfresfi  37726  mettrifi  37817  opidon2OLD  37914  isexid2  37915  grpomndo  37935  elghomlem2OLD  37946  rngoidmlem  37996  rngoueqz  38000  iscringd  38058  cdlemk35s  41056  cdlemk39s  41058  cdlemk42  41060  uzindd  42090  mzpadd  42855  mzpmul  42856  mzpcompact2  42869  dford3lem2  43144  aomclem6  43176  cnsrexpcl  43282  ensucne0OLD  43647  pr2cv  43665  relexpss1d  43822  iunrelexpmin1  43825  iunrelexpmin2  43829  tfindsd  44327  nzin  44435  axc11next  44523  iotavalsb  44550  ssdec  45209  fperiodmullem  45428  monoordxrv  45603  fmul01  45704  fmulcl  45705  fmuldfeqlem1  45706  fmuldfeq  45707  iblspltprt  46095  itgspltprt  46101  stoweidlem2  46124  stoweidlem3  46125  stoweidlem6  46128  stoweidlem8  46130  stoweidlem17  46139  stoweidlem19  46141  stoweidlem21  46143  stoweidlem26  46148  stoweidlem31  46153  stoweidlem43  46165  fourierdlem42  46271  funressnfv  47167  eu2ndop1stv  47249  afv0fv0  47273  afv0nbfvbi  47275  funressnbrafv2  47368  funbrafv2  47371  nelbrim  47399  ssfz12  47438  smonoord  47495  iccpartiltu  47546  iccpartigtl  47547  iccelpart  47557  icceuelpart  47560  fargshiftf  47564  fargshiftf1  47565  fargshiftfo  47566  sprel  47608  sprsymrelf1lem  47615  sprsymrelfolem2  47617  prproropf1olem4  47630  lighneallem4  47734  mogoldbblem  47844  fpprnn  47854  fpprwppr  47863  fpprwpprb  47864  sbgoldbwt  47901  bgoldbtbndlem2  47930  bgoldbtbndlem4  47932  tgoldbach  47941  grimprop  48007  grlimprop  48108  grilcbri2  48135  upwlkwlk  48263  clcllaw  48315  intop  48327  clintop  48332  assintop  48333  assintopcllaw  48336  lmod0rng  48353  ztprmneprm  48471  scmsuppss  48495  ply1mulgsumlem1  48511  ply1mulgsumlem2  48512  lcoel0  48553  ellcoellss  48560  lindslinindsimp2lem5  48587  ldepspr  48598  flnn0div2ge  48658  nnolog2flm1  48715  blengt1fldiv2p1  48718  dignn0flhalf  48743  naryfvalelfv  48757  0aryfvalelfv  48760  fv1arycl  48762  fv2arycl  48773