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  679  axc16i  2466  mo4  2592  sbcn1  3796  sbcim1  3797  sbcbi1  3801  sbcel21v  3811  sbccomlem  3822  csbie2df  4396  elimasni  6077  sotri  6111  unixpid  6267  f0rn0  6745  f1ocnv  6815  funbrfv  6911  elfvmptrab1w  6999  f1dom3el3dif  7249  oprabidw  7423  oprabid  7424  oprabv  7452  ndmovordi  7583  elovmporab  7638  elovmporab1w  7639  elovmporab1  7640  elovmpt3rab1  7652  limomss  7847  unielxp  8004  bropfvvvvlem  8065  f1o2ndf1  8096  smogt  8333  tfrlem1  8341  oawordeulem  8518  omass  8544  ecopovtrn  8797  mapfvd  8857  findcard2d  9131  ssfi  9137  f1domfi  9145  php  9171  unxpdom  9199  findcard3  9223  isfinite2  9238  fsuppimp  9311  fsuppunfi  9331  fsuppunbi  9332  fsuppres  9336  infsupprpr  9449  cantnfval2  9621  cantnfle  9623  cantnfp1lem3  9632  cantnflem1  9641  cnfcom  9652  rankr1ai  9753  rankonidlem  9783  rankxplim2  9835  oncard  9915  ficardom  9916  cardne  9920  acnnum  10005  alephord2i  10030  cardaleph  10042  aceq3lem  10073  dfac5lem5  10080  dfac12lem3  10099  ackbij1lem16  10187  cfslb  10220  cfslb2n  10222  cfsmolem  10224  fin4i  10252  infpssr  10262  fin1a2lem6  10359  axdc3lem2  10405  axcclem  10411  ttukeylem6  10468  fodomb  10480  gchi  10579  pwfseq  10619  inawina  10645  wunfi  10676  inar1  10730  ltexnq  10930  ltbtwnnq  10933  ltexprlem4  10994  ltexpri  10998  prlem936  11002  suplem1pr  11007  suplem2pr  11008  recexsrlem  11058  mulgt0sr  11060  map2psrpr  11065  supsr  11067  eqlei  11290  eqlei2  11291  ledivp1i  12114  nnind  12225  nnmulcl  12231  nn0ge2m1nn  12548  nnnegz  12568  ublbneg  12931  xmulasslem  13285  ixxssixx  13360  iccshftri  13488  iccshftli  13490  iccdili  13492  icccntri  13494  elfz1b  13595  fzo1fzo0n0  13718  elfzonlteqm1  13744  elfzo0l  13759  ssfzo12  13762  fzoopth  13765  elfzo1elm1fzo0  13771  elfzr  13784  elfzlmr  13785  zmodidfzoimp  13908  mptnn0fsuppr  14009  seqp1  14026  seqcl2  14030  seqfveq2  14034  seqshft2  14038  monoord  14042  seqsplit  14045  seqcaopr3  14047  seqf1olem2a  14050  seqf1o  14053  seqid2  14058  seqhomo  14059  hashf1rn  14362  hashinfxadd  14395  hashf1lem2  14466  seqcoll  14474  hash2pr  14479  pr2pwpr  14489  hashge2el2difr  14491  hash3tr  14501  fi1uzind  14517  brfi1indALT  14520  elovmptnn0wrd  14569  swrdswrd  14715  pfxccatin12lem2a  14737  swrdccat  14745  swrdccatin1d  14753  swrdccatin2d  14754  repswccat  14796  cshwidxmod  14813  relexpsucnnr  15035  rtrclreclem3  15070  rtrclreclem4  15071  dfrtrcl2  15072  relexpindlem  15073  relexpind  15074  rtrclind  15075  cjre  15149  climeu  15565  climub  15672  fsum2d  15781  fsumabs  15812  fsumrlim  15822  fsumo1  15823  fsumiun  15832  prodfn0  15907  prodfrec  15908  ntrivcvg  15910  fprodabs  15987  fprod2d  15994  fprodefsum  16108  ruclem9  16253  dvdsmod0  16275  p1modz1  16276  dvdsmodexp  16277  dvdsabseq  16330  mod2eq1n2dvds  16364  mulsucdiv2z  16370  nno  16399  nn0o  16400  sadcadd  16475  sadadd2  16477  saddisjlem  16481  smuval2  16499  smupval  16505  smueqlem  16507  smumullem  16509  dfgcd2  16563  lcmgcdlem  16623  lcmftp  16653  exprmfct  16722  eulerthlem2  16800  dvdsprmpweqnn  16904  dvdsprmpweqle  16905  pcmpt  16911  vdwlem10  17009  cshwsidrepsw  17112  cshwshashlem1  17114  prmlem1a  17125  setsn0fun  17192  ressval3d  17265  mreexexd  17663  letsr  18608  insubm  18835  ghmghmrn  19258  pmtrfrn  19481  pmtr3ncom  19498  gsmtrcl  19539  psgnsn  19543  sylow1lem1  19621  efginvrel2  19750  efgsrel  19757  cntzcmnss  19864  gsum2dlem2  19994  telgsumfzs  20012  dprdval  20028  ablfac1eulem  20097  pgpfac1  20105  pgpfac  20109  srgpcomp  20247  ringrng  20314  ring1ne0  20328  rngimf1o  20482  rngimrnghm  20483  rngimcnv  20484  0ringnnzr  20554  zrhpsgnelbas  21626  psgndiflemA  21633  mplcoe1  22070  mplcoe3  22071  mplcoe5lem  22072  mplcoe5  22073  mpfaddcl  22146  mpfmulcl  22147  coe1ae0  22258  coe1fzgsumd  22347  gsummoncoe1  22351  pf1addcl  22396  pf1mulcl  22397  evl1gsumd  22400  mamufacex  22436  mat0dimcrng  22510  mavmulsolcl  22591  mdetunilem9  22660  cramerlem3  22729  pmatcollpw3fi1  22828  pm2mpfo  22854  chmaidscmat  22888  chfacfscmul0  22898  chfacfpmmul0  22902  cpmadugsumlemF  22916  tg2  23005  neindisj2  23163  neiptopnei  23172  t1t0  23388  fiuncmp  23444  hmeof1o  23804  ist1-5lem  23860  t1r0  23861  alexsublem  24084  imasdsf1olem  24413  tgioo  24836  fsumcn  24912  voliunlem3  25594  itgfsum  25869  dvbsss  25944  dvmptfsum  26017  dvfsumlem2  26069  dvfsumlem4  26071  plyco  26281  dgrcolem1  26313  dgrco  26315  dvntaylp  26411  taylthlem1  26413  jensen  27030  bposlem5  27329  lgsqrmodndvds  27394  gausslemma2dlem0i  27405  gausslemma2dlem4  27410  lgsquad2lem2  27426  2lgslem3  27445  2lgs  27448  2lgsoddprm  27457  dchrisum0flb  27551  pntpbnd1  27627  pntlemf  27646  madebdayim  27958  oldbdayim  27959  pw2cut  28530  brbtwn  29046  brcgr  29047  umgrnloopv  29253  umgrnloop  29255  usgrnloopvALT  29348  usgrnloopALT  29350  usgredg2vlem2  29373  subgrprop  29420  uvtxnbgrvtx  29540  cusgrsize2inds  29600  rgrprop  29707  rusgrprop  29709  wlkprop  29758  wlkvtxeledg  29770  wlkeq  29780  wlkl1loop  29784  wlk1walk  29785  uspgr2wlkeqi  29794  wlkreslem  29814  wlkres  29815  redwlk  29817  lfgrwlknloop  29834  2pthnloop  29877  usgr2trlncl  29906  usgr2pth  29910  clwlkcompim  29926  clwlkcompbp  29928  uspgrn2crct  29954  crctcshwlkn0  29967  wwlknp  29989  wwlkswwlksn  30011  wlkiswwlks2lem4  30018  wlkiswwlks2  30021  wlklnwwlkln2lem  30028  wwlksnext  30039  wwlksnextbi  30040  wwlksnredwwlkn0  30042  wwlksnextwrd  30043  clwlkclwwlklem2a  30146  clwlkclwwlklem2  30148  clwlkclwwlkflem  30152  clwwisshclwws  30163  clwwlknp  30185  clwwlknwwlksn  30186  clwwlkwwlksb  30202  clwwlkext2edg  30204  umgrhashecclwwlk  30226  clwwlknun  30260  1pthond  30292  upgr3v3e3cycl  30328  upgr4cycl4dv4e  30333  eupth2  30387  3vfriswmgr  30426  3cyclfrgrrn1  30433  n4cyclfrgr  30439  frgrnbnb  30441  frgrncvvdeqlem3  30449  frgrncvvdeqlem6  30452  frgrncvvdeqlem7  30453  frgrncvvdeqlem8  30454  frgrwopreglem4a  30458  frgrwopreg  30471  frgrregorufr0  30472  frgr2wwlkeqm  30479  2clwwlk2clwwlklem  30494  wlkl0  30515  frgrreggt1  30541  frgrregord013  30543  frgrregord13  30544  frgrogt3nreg  30545  friendshipgt3  30546  friendship  30547  blocn2  30957  cvexchlem  32517  cdj3lem2b  32586  nnindf  32972  gsumwun  33217  domnprodn0  33420  issgon  34381  sitgclg  34600  sseqp1  34653  bnj938  35196  bnj964  35202  bnj1052  35234  bnj1125  35251  onvf1odlem4  35413  subfacp1lem6  35499  cvmliftlem7  35605  cvmliftlem10  35608  mclsrcl  35875  pprodss4v  36196  segleantisym  36429  rankeq1o  36485  bj-restv  37549  iooelexlt  37820  relowlssretop  37821  rdgeqoa  37828  matunitlindflem1  38079  poimirlem22  38105  poimirlem25  38108  poimirlem28  38111  poimirlem31  38114  mblfinlem3  38122  mbfresfi  38129  mettrifi  38220  opidon2OLD  38317  isexid2  38318  grpomndo  38338  elghomlem2OLD  38349  rngoidmlem  38399  rngoueqz  38403  iscringd  38461  cdlemk35s  41525  cdlemk39s  41527  cdlemk42  41529  uzindd  42559  mzpadd  43283  mzpmul  43284  mzpcompact2  43297  dford3lem2  43568  aomclem6  43600  cnsrexpcl  43706  ensucne0OLD  44070  pr2cv  44088  relexpss1d  44245  iunrelexpmin1  44248  iunrelexpmin2  44252  tfindsd  44750  nzin  44858  axc11next  44946  iotavalsb  44973  ssdec  45630  fperiodmullem  45846  monoordxrv  46019  fmul01  46120  fmulcl  46121  fmuldfeqlem1  46122  fmuldfeq  46123  iblspltprt  46511  itgspltprt  46517  stoweidlem2  46540  stoweidlem3  46541  stoweidlem6  46544  stoweidlem8  46546  stoweidlem17  46555  stoweidlem19  46557  stoweidlem21  46559  stoweidlem26  46564  stoweidlem31  46569  stoweidlem43  46581  fourierdlem42  46687  funressnfv  47601  eu2ndop1stv  47683  afv0fv0  47707  afv0nbfvbi  47709  funressnbrafv2  47802  funbrafv2  47805  nelbrim  47833  ssfz12  47872  smonoord  47935  iccpartiltu  47992  iccpartigtl  47993  iccelpart  48003  icceuelpart  48006  fargshiftf  48010  fargshiftf1  48011  fargshiftfo  48012  sprel  48054  sprsymrelf1lem  48061  sprsymrelfolem2  48063  prproropf1olem4  48076  lighneallem4  48183  mogoldbblem  48306  fpprnn  48316  fpprwppr  48325  fpprwpprb  48326  sbgoldbwt  48363  bgoldbtbndlem2  48392  bgoldbtbndlem4  48394  tgoldbach  48403  grimprop  48469  grlimprop  48570  grilcbri2  48597  upwlkwlk  48725  clcllaw  48777  intop  48789  clintop  48794  assintop  48795  assintopcllaw  48798  lmod0rng  48815  ztprmneprm  48933  scmsuppss  48957  ply1mulgsumlem1  48972  ply1mulgsumlem2  48973  lcoel0  49014  ellcoellss  49021  lindslinindsimp2lem5  49048  ldepspr  49059  flnn0div2ge  49119  nnolog2flm1  49176  blengt1fldiv2p1  49179  dignn0flhalf  49204  naryfvalelfv  49218  0aryfvalelfv  49221  fv1arycl  49223  fv2arycl  49234