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 ⊢ (𝜓 → 𝜒)

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  anabsi5  682  axc16i  2466  mo4  2592  sbcn1  3791  sbcim1  3792  sbcbi1  3796  sbcel21v  3806  sbccomlem  3817  csbie2df  4401  elimasni  6085  sotri  6119  unixpid  6280  f0rn0  6759  f1ocnv  6829  funbrfv  6925  elfvmptrab1w  7013  f1dom3el3dif  7265  oprabidw  7443  oprabid  7444  oprabv  7472  ndmovordi  7604  elovmporab  7659  elovmporab1w  7660  elovmporab1  7661  elovmpt3rab1  7673  limomss  7871  unielxp  8028  bropfvvvvlem  8091  f1o2ndf1  8122  smogt  8359  tfrlem1  8367  oawordeulem  8546  omass  8572  ecopovtrn  8825  mapfvd  8891  findcard2d  9166  ssfi  9172  f1domfi  9180  php  9206  unxpdom  9234  findcard3  9258  isfinite2  9274  fsuppimp  9344  fsuppunfi  9364  fsuppunbi  9365  fsuppres  9369  infsupprpr  9482  cantnfval2  9654  cantnfle  9656  cantnfp1lem3  9665  cantnflem1  9674  cnfcom  9685  rankr1ai  9788  rankonidlem  9819  rankxplim2  9878  oncard  10022  ficardom  10023  cardne  10027  acnnum  10112  alephord2i  10137  cardaleph  10149  aceq3lem  10180  dfac5lem5  10187  dfac12lem3  10205  ackbij1lem16  10293  cfslb  10325  cfslb2n  10327  cfsmolem  10329  fin4i  10357  infpssr  10367  fin1a2lem6  10464  axdc3lem2  10510  axcclem  10516  ttukeylem6  10573  fodomb  10586  gchi  10690  pwfseq  10730  inawina  10756  wunfi  10787  inar1  10841  ltexnq  11041  ltbtwnnq  11044  ltexprlem4  11105  ltexpri  11109  prlem936  11113  suplem1pr  11118  suplem2pr  11119  recexsrlem  11169  mulgt0sr  11171  map2psrpr  11176  supsr  11178  eqlei  11401  eqlei2  11402  ledivp1i  12223  nnind  12334  nnmulcl  12340  nn0ge2m1nn  12657  nnnegz  12677  ublbneg  13041  xmulasslem  13396  ixxssixx  13471  iccshftri  13599  iccshftli  13601  iccdili  13603  icccntri  13605  elfz1b  13707  fzo1fzo0n0  13830  elfzonlteqm1  13856  elfzo0l  13871  ssfzo12  13874  fzoopth  13877  elfzo1elm1fzo0  13883  elfzr  13896  elfzlmr  13897  zmodidfzoimp  14021  mptnn0fsuppr  14122  seqp1  14139  seqcl2  14143  seqfveq2  14147  seqshft2  14151  monoord  14155  seqsplit  14158  seqcaopr3  14160  seqf1olem2a  14163  seqf1o  14166  seqid2  14171  seqhomo  14172  hashf1rn  14476  hashinfxadd  14509  hashf1lem2  14581  seqcoll  14589  hash2pr  14594  pr2pwpr  14604  hashge2el2difr  14606  hash3tr  14616  fi1uzind  14632  brfi1indALT  14635  elovmptnn0wrd  14684  swrdswrd  14834  pfxccatin12lem2a  14856  swrdccat  14864  swrdccatin1d  14872  swrdccatin2d  14873  repswccat  14917  cshwidxmod  14934  relexpsucnnr  15158  rtrclreclem3  15193  rtrclreclem4  15194  dfrtrcl2  15195  relexpindlem  15196  relexpind  15197  rtrclind  15198  cjre  15286  climeu  15702  climub  15809  fsum2d  15917  fsumabs  15948  fsumrlim  15958  fsumo1  15959  fsumiun  15968  prodfn0  16043  prodfrec  16044  ntrivcvg  16046  fprodabs  16121  fprod2d  16128  fprodefsum  16241  ruclem9  16386  dvdsmod0  16408  p1modz1  16409  dvdsmodexp  16410  dvdsabseq  16463  mod2eq1n2dvds  16497  mulsucdiv2z  16503  nno  16532  nn0o  16533  sadcadd  16608  sadadd2  16610  saddisjlem  16614  smuval2  16632  smupval  16638  smueqlem  16640  smumullem  16642  dfgcd2  16699  lcmgcdlem  16761  lcmftp  16791  exprmfct  16860  eulerthlem2  16939  dvdsprmpweqnn  17043  dvdsprmpweqle  17044  pcmpt  17050  vdwlem10  17148  cshwsidrepsw  17251  cshwshashlem1  17253  prmlem1a  17264  setsn0fun  17331  ressval3d  17404  mreexexd  17802  letsr  18747  insubm  18994  ghmghmrn  19429  pmtrfrn  19652  pmtr3ncom  19669  gsmtrcl  19710  psgnsn  19714  sylow1lem1  19792  efginvrel2  19921  efgsrel  19928  cntzcmnss  20035  gsum2dlem2  20165  telgsumfzs  20183  dprdval  20199  ablfac1eulem  20268  pgpfac1  20276  pgpfac  20280  srgpcomp  20424  ringrng  20494  ring1ne0  20510  rngimf1o  20664  rngimrnghm  20665  rngimcnv  20666  0ringnnzr  20756  zrhpsgnelbas  21880  psgndiflemA  21887  mplcoe1  22326  mplcoe3  22327  mplcoe5lem  22328  mplcoe5  22329  mpfaddcl  22402  mpfmulcl  22403  coe1ae0  22514  coe1fzgsumd  22602  gsummoncoe1  22606  pf1addcl  22651  pf1mulcl  22652  evl1gsumd  22655  mamufacex  22691  mat0dimcrng  22765  mavmulsolcl  22846  mdetunilem9  22915  matunitlindflem1  22974  cramerlem3  22987  pmatcollpw3fi1  23086  pm2mpfo  23112  chmaidscmat  23146  chfacfscmul0  23156  chfacfpmmul0  23160  cpmadugsumlemF  23174  tg2  23263  neindisj2  23421  neiptopnei  23430  t1t0  23646  fiuncmp  23702  hmeof1o  24063  ist1-5lem  24119  t1r0  24120  alexsublem  24343  imasdsf1olem  24672  tgioo  25095  fsumcn  25171  voliunlem3  25853  itgfsum  26127  dvbsss  26202  dvmptfsum  26275  dvfsumlem2  26327  dvfsumlem4  26329  plyco  26540  dgrcolem1  26572  dgrco  26574  dvntaylp  26680  taylthlem1  26682  jensen  27298  bposlem5  27597  lgsqrmodndvds  27662  gausslemma2dlem0i  27673  gausslemma2dlem4  27678  lgsquad2lem2  27694  2lgslem3  27713  2lgs  27716  2lgsoddprm  27725  dchrisum0flb  27819  pntpbnd1  27895  pntlemf  27914  madebdayim  28256  oldbdayim  28257  pw2cut  28828  brbtwn  29459  brcgr  29460  umgrnloopv  29666  umgrnloop  29668  usgrnloopvALT  29764  usgrnloopALT  29766  usgredg2vlem2  29789  subgrprop  29836  uvtxnbgrvtx  29956  cusgrsize2inds  30016  rgrprop  30123  rusgrprop  30125  wlkprop  30174  wlkvtxeledg  30186  wlkeq  30196  wlkl1loop  30200  wlk1walk  30201  uspgr2wlkeqi  30210  wlkreslem  30230  wlkres  30231  redwlk  30233  lfgrwlknloop  30254  2pthnloop  30299  usgr2trlncl  30328  usgr2pth  30332  clwlkcompim  30349  clwlkcompbp  30351  uspgrn2crct  30379  crctcshwlkn0  30392  wwlknp  30414  wwlkswwlksn  30436  wlkiswwlks2lem4  30443  wlkiswwlks2  30446  wlklnwwlkln2lem  30453  wwlksnext  30464  wwlksnextbi  30465  wwlksnredwwlkn0  30467  wwlksnextwrd  30468  clwlkclwwlklem2a  30571  clwlkclwwlklem2  30573  clwlkclwwlkflem  30577  clwwisshclwws  30588  clwwlknp  30610  clwwlknwwlksn  30611  clwwlkwwlksb  30627  clwwlkext2edg  30629  umgrhashecclwwlk  30651  clwwlknun  30685  1pthond  30717  upgr3v3e3cycl  30763  upgr4cycl4dv4e  30768  eupth2  30822  3vfriswmgr  30861  3cyclfrgrrn1  30868  n4cyclfrgr  30874  frgrnbnb  30876  frgrncvvdeqlem3  30884  frgrncvvdeqlem6  30887  frgrncvvdeqlem7  30888  frgrncvvdeqlem8  30889  frgrwopreglem4a  30893  frgrwopreg  30906  frgrregorufr0  30907  frgr2wwlkeqm  30914  2clwwlk2clwwlklem  30929  wlkl0  30950  frgrreggt1  30976  frgrregord013  30978  frgrregord13  30979  frgrogt3nreg  30980  friendshipgt3  30981  friendship  30982  blocn2  31392  cvexchlem  32952  cdj3lem2b  33021  nnindf  33393  gsumwun  33619  domnprodn0  33821  issgon  34737  sitgclg  34957  sseqp1  35010  bnj938  35550  bnj964  35556  bnj1052  35588  bnj1125  35605  onvf1odlem4  35858  subfacp1lem6  35919  cvmliftlem7  36025  cvmliftlem10  36028  mclsrcl  36295  pprodss4v  36616  segleantisym  36850  rankeq1o  36902  bj-restv  37984  iooelexlt  38253  relowlssretop  38254  rdgeqoa  38261  poimirlem22  38528  poimirlem25  38531  poimirlem28  38534  poimirlem31  38537  mblfinlem3  38545  mbfresfi  38552  findcard4  38600  mettrifi  38659  opidon2OLD  38756  isexid2  38757  grpomndo  38777  elghomlem2OLD  38788  rngoidmlem  38838  rngoueqz  38842  iscringd  38900  cdlemk35s  41962  cdlemk39s  41964  cdlemk42  41966  uzindd  42996  mzpadd  43702  mzpmul  43703  mzpcompact2  43716  dford3lem2  43987  aomclem6  44019  cnsrexpcl  44125  ensucne0OLD  44489  pr2cv  44507  relexpss1d  44664  iunrelexpmin1  44667  iunrelexpmin2  44671  tfindsd  45167  nzin  45261  axc11next  45349  iotavalsb  45376  ssdec  46046  fperiodmullem  46262  monoordxrv  46435  fmul01  46536  fmulcl  46537  fmuldfeqlem1  46538  fmuldfeq  46539  iblspltprt  46927  itgspltprt  46933  stoweidlem2  46956  stoweidlem3  46957  stoweidlem6  46960  stoweidlem8  46962  stoweidlem17  46971  stoweidlem19  46973  stoweidlem21  46975  stoweidlem26  46980  stoweidlem31  46985  stoweidlem43  46997  fourierdlem42  47103  funressnfv  48057  eu2ndop1stv  48139  afv0fv0  48163  afv0nbfvbi  48165  funressnbrafv2  48258  funbrafv2  48261  nelbrim  48289  ssfz12  48328  smonoord  48391  iccpartiltu  48448  iccpartigtl  48449  iccelpart  48459  icceuelpart  48462  fargshiftf  48466  fargshiftf1  48467  fargshiftfo  48468  sprel  48510  sprsymrelf1lem  48517  sprsymrelfolem2  48519  prproropf1olem4  48532  lighneallem4  48639  mogoldbblem  48762  fpprnn  48772  fpprwppr  48781  fpprwpprb  48782  sbgoldbwt  48819  bgoldbtbndlem2  48848  bgoldbtbndlem4  48850  tgoldbach  48859  grimprop  48925  grlimprop  49026  grilcbri2  49053  upwlkwlk  49181  clcllaw  49232  intop  49244  clintop  49249  assintop  49250  assintopcllaw  49253  lmod0rng  49270  ztprmneprm  49403  scmsuppss  49427  ply1mulgsumlem1  49442  ply1mulgsumlem2  49443  lcoel0  49484  ellcoellss  49491  lindslinindsimp2lem5  49518  ldepspr  49529  flnn0div2ge  49589  nnolog2flm1  49646  blengt1fldiv2p1  49649  dignn0flhalf  49674  naryfvalelfv  49688  0aryfvalelfv  49691  fv1arycl  49693  fv2arycl  49704