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  2467  mo4  2593  sbcn1  3794  sbcim1  3795  sbcbi1  3799  sbcel21v  3809  sbccomlem  3820  csbie2df  4404  elimasni  6091  sotri  6125  unixpid  6286  f0rn0  6764  f1ocnv  6834  funbrfv  6930  elfvmptrab1w  7018  f1dom3el3dif  7270  oprabidw  7448  oprabid  7449  oprabv  7477  ndmovordi  7609  elovmporab  7664  elovmporab1w  7665  elovmporab1  7666  elovmpt3rab1  7678  limomss  7871  unielxp  8028  bropfvvvvlem  8092  f1o2ndf1  8123  smogt  8360  tfrlem1  8368  oawordeulem  8545  omass  8571  ecopovtrn  8824  mapfvd  8890  findcard2d  9165  ssfi  9171  f1domfi  9179  php  9205  unxpdom  9233  findcard3  9257  isfinite2  9272  fsuppimp  9342  fsuppunfi  9362  fsuppunbi  9363  fsuppres  9367  infsupprpr  9480  cantnfval2  9652  cantnfle  9654  cantnfp1lem3  9663  cantnflem1  9672  cnfcom  9683  rankr1ai  9784  rankonidlem  9814  rankxplim2  9866  oncard  9969  ficardom  9970  cardne  9974  acnnum  10059  alephord2i  10084  cardaleph  10096  aceq3lem  10127  dfac5lem5  10134  dfac12lem3  10152  ackbij1lem16  10240  cfslb  10272  cfslb2n  10274  cfsmolem  10276  fin4i  10304  infpssr  10314  fin1a2lem6  10411  axdc3lem2  10457  axcclem  10463  ttukeylem6  10520  fodomb  10533  gchi  10637  pwfseq  10677  inawina  10703  wunfi  10734  inar1  10788  ltexnq  10988  ltbtwnnq  10991  ltexprlem4  11052  ltexpri  11056  prlem936  11060  suplem1pr  11065  suplem2pr  11066  recexsrlem  11116  mulgt0sr  11118  map2psrpr  11123  supsr  11125  eqlei  11348  eqlei2  11349  ledivp1i  12168  nnind  12279  nnmulcl  12285  nn0ge2m1nn  12602  nnnegz  12622  ublbneg  12986  xmulasslem  13341  ixxssixx  13416  iccshftri  13544  iccshftli  13546  iccdili  13548  icccntri  13550  elfz1b  13652  fzo1fzo0n0  13775  elfzonlteqm1  13801  elfzo0l  13816  ssfzo12  13819  fzoopth  13822  elfzo1elm1fzo0  13828  elfzr  13841  elfzlmr  13842  zmodidfzoimp  13966  mptnn0fsuppr  14067  seqp1  14084  seqcl2  14088  seqfveq2  14092  seqshft2  14096  monoord  14100  seqsplit  14103  seqcaopr3  14105  seqf1olem2a  14108  seqf1o  14111  seqid2  14116  seqhomo  14117  hashf1rn  14420  hashinfxadd  14453  hashf1lem2  14525  seqcoll  14533  hash2pr  14538  pr2pwpr  14548  hashge2el2difr  14550  hash3tr  14560  fi1uzind  14576  brfi1indALT  14579  elovmptnn0wrd  14628  swrdswrd  14778  pfxccatin12lem2a  14800  swrdccat  14808  swrdccatin1d  14816  swrdccatin2d  14817  repswccat  14861  cshwidxmod  14878  relexpsucnnr  15102  rtrclreclem3  15137  rtrclreclem4  15138  dfrtrcl2  15139  relexpindlem  15140  relexpind  15141  rtrclind  15142  cjre  15230  climeu  15646  climub  15753  fsum2d  15861  fsumabs  15892  fsumrlim  15902  fsumo1  15903  fsumiun  15912  prodfn0  15987  prodfrec  15988  ntrivcvg  15990  fprodabs  16067  fprod2d  16074  fprodefsum  16187  ruclem9  16332  dvdsmod0  16354  p1modz1  16355  dvdsmodexp  16356  dvdsabseq  16409  mod2eq1n2dvds  16443  mulsucdiv2z  16449  nno  16478  nn0o  16479  sadcadd  16554  sadadd2  16556  saddisjlem  16560  smuval2  16578  smupval  16584  smueqlem  16586  smumullem  16588  dfgcd2  16642  lcmgcdlem  16702  lcmftp  16732  exprmfct  16801  eulerthlem2  16879  dvdsprmpweqnn  16983  dvdsprmpweqle  16984  pcmpt  16990  vdwlem10  17088  cshwsidrepsw  17191  cshwshashlem1  17193  prmlem1a  17204  setsn0fun  17271  ressval3d  17344  mreexexd  17742  letsr  18687  insubm  18933  ghmghmrn  19368  pmtrfrn  19591  pmtr3ncom  19608  gsmtrcl  19649  psgnsn  19653  sylow1lem1  19731  efginvrel2  19860  efgsrel  19867  cntzcmnss  19974  gsum2dlem2  20104  telgsumfzs  20122  dprdval  20138  ablfac1eulem  20207  pgpfac1  20215  pgpfac  20219  srgpcomp  20363  ringrng  20432  ring1ne0  20447  rngimf1o  20601  rngimrnghm  20602  rngimcnv  20603  0ringnnzr  20692  zrhpsgnelbas  21813  psgndiflemA  21820  mplcoe1  22259  mplcoe3  22260  mplcoe5lem  22261  mplcoe5  22262  mpfaddcl  22335  mpfmulcl  22336  coe1ae0  22447  coe1fzgsumd  22535  gsummoncoe1  22539  pf1addcl  22584  pf1mulcl  22585  evl1gsumd  22588  mamufacex  22624  mat0dimcrng  22698  mavmulsolcl  22779  mdetunilem9  22848  matunitlindflem1  22907  cramerlem3  22920  pmatcollpw3fi1  23019  pm2mpfo  23045  chmaidscmat  23079  chfacfscmul0  23089  chfacfpmmul0  23093  cpmadugsumlemF  23107  tg2  23196  neindisj2  23354  neiptopnei  23363  t1t0  23579  fiuncmp  23635  hmeof1o  23996  ist1-5lem  24052  t1r0  24053  alexsublem  24276  imasdsf1olem  24605  tgioo  25028  fsumcn  25104  voliunlem3  25786  itgfsum  26061  dvbsss  26136  dvmptfsum  26209  dvfsumlem2  26261  dvfsumlem4  26263  plyco  26474  dgrcolem1  26506  dgrco  26508  dvntaylp  26614  taylthlem1  26616  jensen  27233  bposlem5  27532  lgsqrmodndvds  27597  gausslemma2dlem0i  27608  gausslemma2dlem4  27613  lgsquad2lem2  27629  2lgslem3  27648  2lgs  27651  2lgsoddprm  27660  dchrisum0flb  27754  pntpbnd1  27830  pntlemf  27849  madebdayim  28161  oldbdayim  28162  pw2cut  28733  brbtwn  29364  brcgr  29365  umgrnloopv  29571  umgrnloop  29573  usgrnloopvALT  29669  usgrnloopALT  29671  usgredg2vlem2  29694  subgrprop  29741  uvtxnbgrvtx  29861  cusgrsize2inds  29921  rgrprop  30028  rusgrprop  30030  wlkprop  30079  wlkvtxeledg  30091  wlkeq  30101  wlkl1loop  30105  wlk1walk  30106  uspgr2wlkeqi  30115  wlkreslem  30135  wlkres  30136  redwlk  30138  lfgrwlknloop  30159  2pthnloop  30204  usgr2trlncl  30233  usgr2pth  30237  clwlkcompim  30254  clwlkcompbp  30256  uspgrn2crct  30284  crctcshwlkn0  30297  wwlknp  30319  wwlkswwlksn  30341  wlkiswwlks2lem4  30348  wlkiswwlks2  30351  wlklnwwlkln2lem  30358  wwlksnext  30369  wwlksnextbi  30370  wwlksnredwwlkn0  30372  wwlksnextwrd  30373  clwlkclwwlklem2a  30476  clwlkclwwlklem2  30478  clwlkclwwlkflem  30482  clwwisshclwws  30493  clwwlknp  30515  clwwlknwwlksn  30516  clwwlkwwlksb  30532  clwwlkext2edg  30534  umgrhashecclwwlk  30556  clwwlknun  30590  1pthond  30622  upgr3v3e3cycl  30668  upgr4cycl4dv4e  30673  eupth2  30727  3vfriswmgr  30766  3cyclfrgrrn1  30773  n4cyclfrgr  30779  frgrnbnb  30781  frgrncvvdeqlem3  30789  frgrncvvdeqlem6  30792  frgrncvvdeqlem7  30793  frgrncvvdeqlem8  30794  frgrwopreglem4a  30798  frgrwopreg  30811  frgrregorufr0  30812  frgr2wwlkeqm  30819  2clwwlk2clwwlklem  30834  wlkl0  30855  frgrreggt1  30881  frgrregord013  30883  frgrregord13  30884  frgrogt3nreg  30885  friendshipgt3  30886  friendship  30887  blocn2  31297  cvexchlem  32857  cdj3lem2b  32926  nnindf  33298  gsumwun  33524  domnprodn0  33726  issgon  34641  sitgclg  34861  sseqp1  34914  bnj938  35454  bnj964  35460  bnj1052  35492  bnj1125  35509  onvf1odlem4  35711  subfacp1lem6  35772  cvmliftlem7  35878  cvmliftlem10  35881  mclsrcl  36148  pprodss4v  36469  segleantisym  36703  rankeq1o  36759  bj-restv  37853  iooelexlt  38124  relowlssretop  38125  rdgeqoa  38132  poimirlem22  38399  poimirlem25  38402  poimirlem28  38405  poimirlem31  38408  mblfinlem3  38416  mbfresfi  38423  findcard4  38471  mettrifi  38515  opidon2OLD  38612  isexid2  38613  grpomndo  38633  elghomlem2OLD  38644  rngoidmlem  38694  rngoueqz  38698  iscringd  38756  cdlemk35s  41818  cdlemk39s  41820  cdlemk42  41822  uzindd  42852  mzpadd  43591  mzpmul  43592  mzpcompact2  43605  dford3lem2  43876  aomclem6  43908  cnsrexpcl  44014  ensucne0OLD  44378  pr2cv  44396  relexpss1d  44553  iunrelexpmin1  44556  iunrelexpmin2  44560  tfindsd  45056  nzin  45150  axc11next  45238  iotavalsb  45265  ssdec  45928  fperiodmullem  46144  monoordxrv  46317  fmul01  46418  fmulcl  46419  fmuldfeqlem1  46420  fmuldfeq  46421  iblspltprt  46809  itgspltprt  46815  stoweidlem2  46838  stoweidlem3  46839  stoweidlem6  46842  stoweidlem8  46844  stoweidlem17  46853  stoweidlem19  46855  stoweidlem21  46857  stoweidlem26  46862  stoweidlem31  46867  stoweidlem43  46879  fourierdlem42  46985  funressnfv  47939  eu2ndop1stv  48021  afv0fv0  48045  afv0nbfvbi  48047  funressnbrafv2  48140  funbrafv2  48143  nelbrim  48171  ssfz12  48210  smonoord  48273  iccpartiltu  48330  iccpartigtl  48331  iccelpart  48341  icceuelpart  48344  fargshiftf  48348  fargshiftf1  48349  fargshiftfo  48350  sprel  48392  sprsymrelf1lem  48399  sprsymrelfolem2  48401  prproropf1olem4  48414  lighneallem4  48521  mogoldbblem  48644  fpprnn  48654  fpprwppr  48663  fpprwpprb  48664  sbgoldbwt  48701  bgoldbtbndlem2  48730  bgoldbtbndlem4  48732  tgoldbach  48741  grimprop  48807  grlimprop  48908  grilcbri2  48935  upwlkwlk  49063  clcllaw  49114  intop  49126  clintop  49131  assintop  49132  assintopcllaw  49135  lmod0rng  49152  ztprmneprm  49285  scmsuppss  49309  ply1mulgsumlem1  49324  ply1mulgsumlem2  49325  lcoel0  49366  ellcoellss  49373  lindslinindsimp2lem5  49400  ldepspr  49411  flnn0div2ge  49471  nnolog2flm1  49528  blengt1fldiv2p1  49531  dignn0flhalf  49556  naryfvalelfv  49570  0aryfvalelfv  49573  fv1arycl  49575  fv2arycl  49586