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  2468  mo4  2594  sbcn1  3794  sbcim1  3795  sbcbi1  3799  sbcel21v  3809  sbccomlem  3821  csbie2df  4404  elimasni  6101  sotri  6133  unixpid  6305  f0rn0  6789  f1ocnv  6859  funbrfv  6956  elfvmptrab1w  7044  f1dom3el3dif  7296  oprabidw  7474  oprabid  7475  oprabv  7503  ndmovordi  7636  elovmporab  7691  elovmporab1w  7692  elovmporab1  7693  elovmpt3rab1  7705  limomss  7906  unielxp  8063  bropfvvvvlem  8127  f1o2ndf1  8160  smogt  8403  tfrlem1  8411  oawordeulem  8590  omass  8616  ecopovtrn  8869  mapfvd  8935  findcard2d  9210  ssfi  9216  f1domfi  9224  php  9250  unxpdom  9278  findcard3  9302  isfinite2  9318  fsuppimp  9388  fsuppunfi  9407  fsuppunbi  9408  fsuppres  9412  infsupprpr  9525  cantnfval2  9697  cantnfle  9699  cantnfp1lem3  9708  cantnflem1  9717  cnfcom  9728  rankr1ai  9833  rankonidlem  9865  rankxplim2  9924  oncard  10068  ficardom  10069  cardne  10073  acnnum  10158  alephord2i  10183  cardaleph  10195  aceq3lem  10226  dfac5lem5  10233  dfac12lem3  10251  ackbij1lem16  10339  cfslb  10371  cfslb2n  10373  cfsmolem  10375  fin4i  10403  infpssr  10413  fin1a2lem6  10510  axdc3lem2  10556  axcclem  10562  ttukeylem6  10619  fodomb  10632  gchi  10736  pwfseq  10776  inawina  10802  wunfi  10833  inar1  10887  ltexnq  11087  ltbtwnnq  11090  ltexprlem4  11151  ltexpri  11155  prlem936  11159  suplem1pr  11164  suplem2pr  11165  recexsrlem  11215  mulgt0sr  11217  map2psrpr  11222  supsr  11224  eqlei  11447  eqlei2  11448  ledivp1i  12269  nnind  12380  nnmulcl  12386  nn0ge2m1nn  12703  nnnegz  12723  ublbneg  13087  xmulasslem  13442  ixxssixx  13517  iccshftri  13645  iccshftli  13647  iccdili  13649  icccntri  13651  elfz1b  13754  fzo1fzo0n0  13877  elfzonlteqm1  13903  elfzo0l  13918  ssfzo12  13921  fzoopth  13924  elfzo1elm1fzo0  13930  elfzr  13943  elfzlmr  13944  zmodidfzoimp  14068  mptnn0fsuppr  14169  seqp1  14186  seqcl2  14190  seqfveq2  14194  seqshft2  14198  monoord  14202  seqsplit  14205  seqcaopr3  14207  seqf1olem2a  14210  seqf1o  14213  seqid2  14218  seqhomo  14219  hashf1rn  14523  hashinfxadd  14556  hashf1lem2  14628  seqcoll  14636  hash2pr  14641  pr2pwpr  14651  hashge2el2difr  14653  hash3tr  14663  fi1uzind  14679  brfi1indALT  14682  elovmptnn0wrd  14731  swrdswrd  14882  pfxccatin12lem2a  14904  swrdccat  14912  swrdccatin1d  14920  swrdccatin2d  14921  repswccat  14965  cshwidxmod  14982  relexpsucnnr  15207  rtrclreclem3  15242  rtrclreclem4  15243  dfrtrcl2  15244  relexpindlem  15245  relexpind  15246  rtrclind  15247  cjre  15335  climeu  15751  climub  15858  fsum2d  15966  fsumabs  15997  fsumrlim  16007  fsumo1  16008  fsumiun  16017  prodfn0  16092  prodfrec  16093  ntrivcvg  16095  fprodabs  16170  fprod2d  16177  fprodefsum  16290  ruclem9  16435  dvdsmod0  16457  p1modz1  16458  dvdsmodexp  16459  dvdsabseq  16512  mod2eq1n2dvds  16546  mulsucdiv2z  16552  nno  16581  nn0o  16582  sadcadd  16657  sadadd2  16659  saddisjlem  16663  smuval2  16681  smupval  16687  smueqlem  16689  smumullem  16691  dfgcd2  16748  lcmgcdlem  16810  lcmftp  16840  exprmfct  16909  eulerthlem2  16988  dvdsprmpweqnn  17092  dvdsprmpweqle  17093  pcmpt  17099  vdwlem10  17197  cshwsidrepsw  17300  cshwshashlem1  17302  prmlem1a  17313  setsn0fun  17380  ressval3d  17453  mreexexd  17851  letsr  18796  insubm  19043  ghmghmrn  19478  pmtrfrn  19702  pmtr3ncom  19719  gsmtrcl  19760  psgnsn  19764  sylow1lem1  19842  efginvrel2  19971  efgsrel  19978  cntzcmnss  20085  gsum2dlem2  20215  telgsumfzs  20233  dprdval  20249  ablfac1eulem  20318  pgpfac1  20326  pgpfac  20330  srgpcomp  20474  ringrng  20544  ring1ne0  20560  rngimf1o  20714  rngimrnghm  20715  rngimcnv  20716  0ringnnzr  20806  zrhpsgnelbas  21930  psgndiflemA  21937  mplcoe1  22376  mplcoe3  22377  mplcoe5lem  22378  mplcoe5  22379  mpfaddcl  22452  mpfmulcl  22453  coe1ae0  22564  coe1fzgsumd  22652  gsummoncoe1  22656  pf1addcl  22701  pf1mulcl  22702  evl1gsumd  22705  mamufacex  22741  mat0dimcrng  22815  mavmulsolcl  22896  mdetunilem9  22965  matunitlindflem1  23024  cramerlem3  23037  pmatcollpw3fi1  23136  pm2mpfo  23162  chmaidscmat  23196  chfacfscmul0  23206  chfacfpmmul0  23210  cpmadugsumlemF  23224  tg2  23313  neindisj2  23471  neiptopnei  23480  t1t0  23696  fiuncmp  23752  hmeof1o  24113  ist1-5lem  24169  t1r0  24170  alexsublem  24393  imasdsf1olem  24722  tgioo  25145  fsumcn  25221  voliunlem3  25903  itgfsum  26177  dvbsss  26252  dvmptfsum  26325  dvfsumlem2  26377  dvfsumlem4  26379  plyco  26590  dgrcolem1  26622  dgrco  26624  dvntaylp  26728  taylthlem1  26730  jensen  27346  bposlem5  27645  lgsqrmodndvds  27710  gausslemma2dlem0i  27721  gausslemma2dlem4  27726  lgsquad2lem2  27742  2lgslem3  27761  2lgs  27764  2lgsoddprm  27773  dchrisum0flb  27867  pntpbnd1  27943  pntlemf  27962  madebdayim  28304  oldbdayim  28305  pw2cut  28876  brbtwn  29507  brcgr  29508  umgrnloopv  29714  umgrnloop  29716  usgrnloopvALT  29812  usgrnloopALT  29814  usgredg2vlem2  29837  subgrprop  29884  uvtxnbgrvtx  30004  cusgrsize2inds  30064  rgrprop  30171  rusgrprop  30173  wlkprop  30222  wlkvtxeledg  30234  wlkeq  30244  wlkl1loop  30248  wlk1walk  30249  uspgr2wlkeqi  30258  wlkreslem  30278  wlkres  30279  redwlk  30281  lfgrwlknloop  30302  2pthnloop  30347  usgr2trlncl  30376  usgr2pth  30380  clwlkcompim  30397  clwlkcompbp  30399  uspgrn2crct  30427  crctcshwlkn0  30440  wwlknp  30462  wwlkswwlksn  30484  wlkiswwlks2lem4  30491  wlkiswwlks2  30494  wlklnwwlkln2lem  30501  wwlksnext  30512  wwlksnextbi  30513  wwlksnredwwlkn0  30515  wwlksnextwrd  30516  clwlkclwwlklem2a  30619  clwlkclwwlklem2  30621  clwlkclwwlkflem  30625  clwwisshclwws  30636  clwwlknp  30658  clwwlknwwlksn  30659  clwwlkwwlksb  30675  clwwlkext2edg  30677  umgrhashecclwwlk  30699  clwwlknun  30733  1pthond  30765  upgr3v3e3cycl  30811  upgr4cycl4dv4e  30816  eupth2  30870  3vfriswmgr  30909  3cyclfrgrrn1  30916  n4cyclfrgr  30922  frgrnbnb  30924  frgrncvvdeqlem3  30932  frgrncvvdeqlem6  30935  frgrncvvdeqlem7  30936  frgrncvvdeqlem8  30937  frgrwopreglem4a  30941  frgrwopreg  30954  frgrregorufr0  30955  frgr2wwlkeqm  30962  2clwwlk2clwwlklem  30977  wlkl0  30998  frgrreggt1  31024  frgrregord013  31026  frgrregord13  31027  frgrogt3nreg  31028  friendshipgt3  31029  friendship  31030  blocn2  31440  cvexchlem  33000  cdj3lem2b  33069  nnindf  33481  gsumwun  33707  domnprodn0  33909  issgon  34825  sitgclg  35044  sseqp1  35097  bnj938  35637  bnj964  35643  bnj1052  35675  bnj1125  35692  onvf1odlem4  36034  subfacp1lem6  36117  cvmliftlem7  36223  cvmliftlem10  36226  mclsrcl  36493  pprodss4v  36824  segleantisym  37058  rankeq1o  37110  bj-restv  38207  iooelexlt  38477  relowlssretop  38478  rdgeqoa  38485  poimirlem22  38752  poimirlem25  38755  poimirlem28  38758  poimirlem31  38761  mblfinlem3  38769  mbfresfi  38776  findcard4  38824  mettrifi  38883  opidon2OLD  38980  isexid2  38981  grpomndo  39001  elghomlem2OLD  39012  rngoidmlem  39062  rngoueqz  39066  iscringd  39124  cdlemk35s  42186  cdlemk39s  42188  cdlemk42  42190  uzindd  43220  mzpadd  43942  mzpmul  43943  mzpcompact2  43956  dford3lem2  44227  aomclem6  44254  cnsrexpcl  44359  ensucne0OLD  44723  pr2cv  44741  relexpss1d  44897  iunrelexpmin1  44900  iunrelexpmin2  44904  tfindsd  45400  nzin  45494  axc11next  45582  iotavalsb  45608  ssdec  46308  fperiodmullem  46524  monoordxrv  46696  fmul01  46797  fmulcl  46798  fmuldfeqlem1  46799  fmuldfeq  46800  iblspltprt  47188  itgspltprt  47194  stoweidlem2  47217  stoweidlem3  47218  stoweidlem6  47221  stoweidlem8  47223  stoweidlem17  47232  stoweidlem19  47234  stoweidlem21  47236  stoweidlem26  47241  stoweidlem31  47246  stoweidlem43  47258  fourierdlem42  47364  funressnfv  48318  eu2ndop1stv  48400  afv0fv0  48424  afv0nbfvbi  48426  funressnbrafv2  48519  funbrafv2  48522  nelbrim  48550  ssfz12  48589  smonoord  48652  iccpartiltu  48709  iccpartigtl  48710  iccelpart  48720  icceuelpart  48723  fargshiftf  48727  fargshiftf1  48728  fargshiftfo  48729  sprel  48771  sprsymrelf1lem  48778  sprsymrelfolem2  48780  prproropf1olem4  48793  lighneallem4  48900  mogoldbblem  49023  fpprnn  49033  fpprwppr  49042  fpprwpprb  49043  sbgoldbwt  49080  bgoldbtbndlem2  49109  bgoldbtbndlem4  49111  tgoldbach  49120  grimprop  49186  grlimprop  49287  grilcbri2  49314  upwlkwlk  49442  clcllaw  49493  intop  49505  clintop  49510  assintop  49511  assintopcllaw  49514  lmod0rng  49531  ztprmneprm  49664  scmsuppss  49688  ply1mulgsumlem1  49703  ply1mulgsumlem2  49704  lcoel0  49745  ellcoellss  49752  lindslinindsimp2lem5  49779  ldepspr  49790  flnn0div2ge  49850  nnolog2flm1  49907  blengt1fldiv2p1  49910  dignn0flhalf  49935  naryfvalelfv  49949  0aryfvalelfv  49952  fv1arycl  49954  fv2arycl  49965