Theorem mpcom 37

Description: Modus ponens inference with commutation of antecedents. (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:  syldan  486  axc16i  2310  sbcn1  3448  sbcim1  3449  sbcbi1  3450  sbcel21v  3464  elimasni  5411  sotri  5442  unixpid  5587  f0rn0  6003  f1ocnv  6062  tz6.12c  6123  funbrfv  6144  funopsn  6319  f1dom3el3dif  6426  oprabid  6576  oprabv  6601  ndmovordi  6723  elovmpt2rab  6778  elovmpt2rab1  6779  elovmpt3rab1  6791  limomss  6962  unielxp  7095  bropfvvvvlem  7143  f1o2ndf1  7172  smogt  7351  tfrlem1  7359  oawordeulem  7521  omass  7547  ecopovtrn  7737  php  8029  unxpdom  8052  findcard2d  8087  findcard3  8088  isfinite2  8103  fsuppimp  8164  fsuppunfi  8178  fsuppunbi  8179  fsuppres  8183  cantnfval2  8449  cantnfle  8451  cantnfp1lem3  8460  cantnflem1  8469  cnfcom  8480  rankr1ai  8544  rankonidlem  8574  rankxplim2  8626  oncard  8669  ficardom  8670  cardne  8674  acnnum  8758  alephord2i  8783  cardaleph  8795  aceq3lem  8826  dfac5lem5  8833  dfac12lem3  8850  cdainf  8897  ackbij1lem16  8940  cfslb  8971  cfslb2n  8973  cfsmolem  8975  fin4i  9003  infpssr  9013  fin1a2lem6  9110  axdc3lem2  9156  axcclem  9162  ttukeylem6  9219  fodomb  9229  gchi  9325  fpwwe2lem5  9335  pwfseqlem4  9363  pwfseq  9365  inawina  9391  wunfi  9422  inar1  9476  ltexnq  9676  ltbtwnnq  9679  ltexprlem4  9740  ltexpri  9744  prlem936  9748  suplem1pr  9753  suplem2pr  9754  recexsrlem  9803  mulgt0sr  9805  map2psrpr  9810  supsr  9812  eqlei  10026  eqlei2  10027  ledivp1i  10828  nnind  10915  nnmulcl  10920  nn0ge2m1nn  11237  nnnegz  11257  ublbneg  11649  xmulasslem  11987  ixxssixx  12060  iccshftri  12178  iccshftli  12180  iccdili  12182  icccntri  12184  fzo1fzo0n0  12386  elfzonlteqm1  12410  ssfzo12  12427  elfzo1elm1fzo0  12435  zmodidfzoimp  12562  mptnn0fsuppr  12661  seqp1  12678  seqcl2  12681  seqfveq2  12685  seqshft2  12689  monoord  12693  seqsplit  12696  seqcaopr3  12698  seqf1olem2a  12701  seqf1o  12704  seqid2  12709  seqhomo  12710  hashf1rn  13004  hashf1rnOLD  13005  hashinfxadd  13035  hashf1lem2  13097  seqcoll  13105  hash2pr  13108  pr2pwpr  13116  hashge2el2difr  13118  hash3tr  13127  fi1uzind  13134  brfi1indALT  13137  fi1uzindOLD  13140  brfi1indALTOLD  13143  elovmptnn0wrd  13203  swrdswrd  13312  swrdccatin12lem2a  13336  swrdccat  13344  swrdccatin1d  13350  swrdccatin2d  13351  swrdccatin12d  13352  repswccat  13383  cshwidxmod  13400  relexpsucnnr  13613  rtrclreclem3  13648  rtrclreclem4  13649  dfrtrcl2  13650  relexpindlem  13651  relexpind  13652  rtrclind  13653  cjre  13727  climeu  14134  climub  14240  fsum2d  14344  fsumabs  14374  fsumrlim  14384  fsumo1  14385  fsumiun  14394  prodfn0  14465  prodfrec  14466  ntrivcvg  14468  fprodabs  14543  fprod2d  14550  fprodefsum  14664  ruclem9  14806  dvdsabseq  14873  mod2eq1n2dvds  14909  mulsucdiv2z  14915  nno  14936  nn0o  14937  sadcadd  15018  sadadd2  15020  saddisjlem  15024  smuval2  15042  smupval  15048  smueqlem  15050  smumullem  15052  dfgcd2  15101  lcmgcdlem  15157  lcmftp  15187  exprmfct  15254  eulerthlem2  15325  dvdsprmpweqnn  15427  dvdsprmpweqle  15428  pcmpt  15434  vdwlem10  15532  cshwsidrepsw  15638  cshwshashlem1  15640  prmlem1a  15651  ressval3d  15764  mreexexd  16131  mreexexdOLD  16132  letsr  17050  ghmghmrn  17502  pmtrfrn  17701  pmtr3ncom  17718  gsmtrcl  17759  psgnsn  17763  sylow1lem1  17836  efginvrel2  17963  efgsrel  17970  cntzcmnss  18069  gsumzoppg  18167  gsum2dlem2  18193  telgsumfzs  18209  dprdval  18225  ablfac1eulem  18294  pgpfac1  18302  pgpfac  18306  srgpcomp  18355  ring1ne0  18414  rimf1o  18557  rimrhm  18558  brric2  18568  0ringnnzr  19090  mplcoe1  19286  mplcoe3  19287  mplcoe5lem  19288  mplcoe5  19289  mpfaddcl  19355  mpfmulcl  19356  coe1ae0  19407  coe1fzgsumd  19493  gsummoncoe1  19495  pf1addcl  19538  pf1mulcl  19539  evl1gsumd  19542  zrhpsgnelbas  19759  psgndiflemA  19766  mamufacex  20014  mat0dimcrng  20095  mavmulsolcl  20176  mdetunilem9  20245  cramerlem3  20314  pmatcollpw3fi1  20412  pm2mpfo  20438  chmaidscmat  20472  chfacfscmul0  20482  chfacfpmmul0  20486  cpmadugsumlemF  20500  tg2  20580  neindisj2  20737  neiptopnei  20746  t1t0  20962  fiuncmp  21017  hmeof1o  21377  ist1-5lem  21433  t1r0  21434  alexsublem  21658  imasdsf1olem  21988  tgioo  22407  fsumcn  22481  voliunlem3  23127  itgfsum  23399  dvbsss  23472  dvmptfsum  23542  dvfsumlem2  23594  dvfsumlem4  23596  plyco  23801  dgrcolem1  23833  dgrco  23835  dvntaylp  23929  taylthlem1  23931  jensen  24515  bposlem5  24813  lgsqrmodndvds  24878  gausslemma2dlem0i  24889  gausslemma2dlem4  24894  lgsquad2lem2  24910  2lgslem3  24929  2lgs  24932  2lgsoddprm  24941  dchrisum0flb  24999  pntpbnd1  25075  pntlemf  25094  brbtwn  25579  brcgr  25580  uhgrstrrepelem  25744  umgrnloopv  25772  umgrnloop  25774  ushgrauhgra  25832  uhgra0v  25839  umisuhgra  25856  usgrac  25880  uslgraf1oedg  25888  uslisushgra  25892  uslisumgra  25893  usisuslgra  25894  elusuhgra  25897  usgra0v  25900  usgranloopv  25907  usgranloop  25908  usgra1v  25919  usgraidx2vlem2  25921  usgrafisindb0  25937  usgrafisindb1  25938  usgrafisinds  25942  usgrafisbase  25943  iscusgra0  25986  cusgrasize2inds  26005  cusgrafi  26010  2mwlk  26049  iswlkg  26052  wlkcpr  26057  edgwlk  26059  trliswlk  26069  2trllemE  26083  usgrwlknloop  26093  pthistrl  26102  spthispth  26103  pthdepisspth  26104  redwlk  26136  wlkdvspth  26138  usgra2adedgspthlem2  26140  usgra2wlkspth  26149  crctistrl  26156  cyclispth  26157  cycliscrct  26158  cyclnspth  26159  cyclispthon  26161  fargshiftf  26164  fargshiftf1  26165  fargshiftfo  26166  usgrcyclnl1  26168  usgrcyclnl2  26169  nvnencycllem  26171  3v3e3cycl1  26172  constr3trllem5  26182  constr3trl  26187  constr3pth  26188  constr3cycl  26189  4cycl4v4e  26194  4cycl4dv4e  26196  cusconngra  26204  wwlknimp  26215  wwlkn0  26217  wlkiswwlk1  26218  wlkiswwlk2lem4  26222  wlkiswwlk2  26225  wlklniswwlkn2  26228  wwlkiswwlkn  26230  2wlkeq  26235  wwlknred  26251  wwlknext  26252  wwlknextbi  26253  wwlknredwwlkn0  26255  wwlkextwrd  26256  wwlkm1edg  26263  wwlkextproplem3  26271  isclwlkg  26283  clwlkswlks  26286  clwwlkprop  26298  clwwlkgt0  26299  clwwlknprop  26300  clwwlknimp  26304  clwlkisclwwlklem2a  26313  clwlkisclwwlklem1  26315  clwwlkext2edg  26330  clwwisshclww  26335  clwwnisshclwwn  26337  usghashecclwwlk  26362  wlklenvclwlk  26366  2spontn0vne  26414  usg2spthonot  26415  usg2spthonot0  26416  usgfidegfi  26437  usgravd00  26446  rgraprop  26455  rusgraprop  26456  rusgrargra  26457  cusgraisrusgra  26465  0eusgraiff0rgracl  26468  rusgrasn  26472  rusgranumwlklem1  26476  eupatrl  26495  eupath2  26507  3vfriswmgra  26532  3cyclfrgrarn1  26539  3cyclfrgrarn  26540  n4cyclfrgra  26545  frgranbnb  26547  frconngra  26548  vdfrgra0  26549  vdn0frgrav2  26550  vdgn0frgrav2  26551  usgn0fidegnn0  26556  frgrancvvdeqlem4  26560  frgrancvvdeqlem7  26563  frgrancvvdeqlemA  26564  frgrancvvdeqlemB  26565  frgrawopreglem4  26574  frgrawopreglem5  26575  frgrawopreg  26576  frgraregorufr0  26579  frgraeu  26581  frg2wot1  26584  frg2woteqm  26586  frg2woteq  26587  frgregordn0  26597  numclwwlkun  26606  numclwwlk8  26642  frgrareggt1  26643  frgrareg  26644  frgraregord013  26645  frgraregord13  26646  frgraogt3nreg  26647  friendshipgt3  26648  friendship  26649  blocn2  27047  cvexchlem  28611  cdj3lem2b  28680  cnvoprab  28886  nnindf  28952  issgon  29513  sitgclg  29731  sseqp1  29784  bnj938  30261  bnj964  30267  bnj1052  30297  bnj1125  30314  subfacp1lem6  30421  cvmliftlem7  30527  cvmliftlem10  30530  mclsrcl  30712  pprodss4v  31161  segleantisym  31392  rankeq1o  31448  bj-restv  32229  iooelexlt  32386  relowlssretop  32387  rdgeqoa  32394  matunitlindflem1  32575  poimirlem22  32601  poimirlem25  32604  poimirlem28  32607  poimirlem31  32610  mblfinlem3  32618  mbfresfi  32626  mettrifi  32723  opidon2OLD  32823  isexid2  32824  grpomndo  32844  elghomlem2OLD  32855  rngoidmlem  32905  rngoueqz  32909  iscringd  32967  cdlemk35s  35243  cdlemk39s  35245  cdlemk42  35247  mzpadd  36319  mzpmul  36320  mzpcompact2  36333  dford3lem2  36612  aomclem6  36647  cnsrexpcl  36754  relexpss1d  37016  iunrelexpmin1  37019  iunrelexpmin2  37023  nzin  37539  axc11next  37629  iotavalsb  37656  ssdec  38293  fperiodmullem  38458  fmul01  38647  fmulcl  38648  fmuldfeqlem1  38649  fmuldfeq  38650  fprodcnlem  38666  iblspltprt  38865  itgspltprt  38871  stoweidlem2  38895  stoweidlem3  38896  stoweidlem6  38899  stoweidlem8  38901  stoweidlem17  38910  stoweidlem19  38912  stoweidlem21  38914  stoweidlem26  38919  stoweidlem31  38924  stoweidlem43  38936  fourierdlem42  39042  eu2ndop1stv  39851  funressnfv  39857  afv0fv0  39878  afv0nbfvbi  39880  smonoord  39944  iccpartiltu  39960  iccpartigtl  39961  iccelpart  39971  icceuelpart  39974  lighneallem4  40065  bgoldbwt  40199  bgoldbtbndlem2  40222  bgoldbtbndlem4  40224  tgoldbach  40232  tgoldbachOLD  40239  ssfz12  40351  fzoopth  40360  elfzr  40364  elfzo0l  40365  elfzlmr  40366  uspgrf1oedg  40403  usgrnloopvALT  40428  usgrnloopALT  40430  usgredg2vlem2  40453  subgrprop  40497  uvtxaisvtx  40615  vtxnbuvtx  40617  uvtxanbgrvtx  40619  cusgrsize2inds  40669  rgrprop  40760  rusgrprop  40762  2m1wlk  40818  1wlkvtxeledg  40828  1wlkeq  40838  1wlkl1loop  40842  1wlk1walk  40843  wlk1wlk  40846  upgrwlkedg  40850  uspgr2wlkeqi  40856  1wlkreslem  40878  1wlkres  40879  red1wlk  40881  lfgr1wlknloop  40898  trlis1wlk  40905  trlf1  40906  PthisTrl  40931  sPthisPth  40932  pthdivtx  40935  2pthnloop  40937  sPthdifv  40939  spthdep  40940  pthdepissPth  40941  usgr2trlncl  40966  usgr2pth  40970  isclWlkb  40980  clwlkis1wlk  40981  clwlk1wlk  40982  clWlkcompim  40987  crctprop  40998  cyclprop  40999  crctisclwlk  41000  cyclisCrct  41005  cyclnsPth  41006  cyclisPthon  41007  uspgrn2crct  41011  crctcsh1wlkn0  41024  wwlknp  41045  wwlkswwlksn  41061  1wlkiswwlks1  41064  1wlkiswwlks2lem4  41069  1wlkiswwlks2  41072  1wlklnwwlkln2lem  41079  wwlksnext  41099  wwlksnextbi  41100  wwlksnredwwlkn0  41102  wwlksnextwrd  41103  clwwlknp  41195  clwwlkclwwlkn  41199  clwlkclwwlklem2a  41207  clwlkclwwlklem2  41209  clwwlksext2edg  41230  clwwisshclwws  41235  clwwnisshclwwsn  41237  umgrhashecclwwlk  41262  clwwlksnun  41281  1pthond  41311  upgr3v3e3cycl  41347  upgr4cycl4dv4e  41352  eupthtrli  41370  eupthi  41371  upgreupthi  41376  eupth2  41407  3vfriswmgr  41448  3cyclfrgrrn1  41455  n4cyclfrgr  41461  frgrnbnb  41463  frgrncvvdeqlem4  41472  frgrncvvdeqlem7  41475  frgrncvvdeqlemA  41476  frgrncvvdeqlemB  41477  frgrwopreglem4  41484  frgrwopreg  41486  frgrregorufr0  41489  frgreu  41491  frgr2wwlk1  41494  frgr2wwlkeqm  41496  fusgr2wsp2nb  41498  frrusgrord0  41503  av-numclwwlk8  41546  av-frgrareggt1  41547  av-frgraregord013  41549  av-frgraregord13  41550  av-frgraogt3nreg  41551  av-friendshipgt3  41552  av-friendship  41553  clcllaw  41617  intop  41629  clintop  41634  assintop  41635  assintopcllaw  41638  lmod0rng  41658  ringrng  41669  rngimf1o  41695  rngimrnghm  41696  ztprmneprm  41918  scmsuppss  41947  ply1mulgsumlem1  41968  ply1mulgsumlem2  41969  lcoel0  42011  ellcoellss  42018  lindslinindsimp2lem5  42045  ldepspr  42056  flnn0div2ge  42121  nnolog2flm1  42182  blengt1fldiv2p1  42185  dignn0flhalf  42210