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

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  681  axc16i  2468  mo4  2594  sbcn1  3797  sbcim1  3798  sbcbi1  3802  sbcel21v  3812  sbccomlem  3823  csbie2df  4409  elimasni  6095  sotri  6129  unixpid  6287  f0rn0  6765  f1ocnv  6835  funbrfv  6931  elfvmptrab1w  7019  f1dom3el3dif  7269  oprabidw  7443  oprabid  7444  oprabv  7472  ndmovordi  7603  elovmporab  7658  elovmporab1w  7659  elovmporab1  7660  elovmpt3rab1  7672  limomss  7868  unielxp  8025  bropfvvvvlem  8087  f1o2ndf1  8118  smogt  8355  tfrlem1  8363  oawordeulem  8540  omass  8566  ecopovtrn  8819  mapfvd  8878  findcard2d  9152  ssfi  9158  f1domfi  9166  php  9192  unxpdom  9220  findcard3  9244  isfinite2  9259  fsuppimp  9329  fsuppunfi  9349  fsuppunbi  9350  fsuppres  9354  infsupprpr  9467  cantnfval2  9639  cantnfle  9641  cantnfp1lem3  9650  cantnflem1  9659  cnfcom  9670  rankr1ai  9771  rankonidlem  9801  rankxplim2  9853  oncard  9947  ficardom  9948  cardne  9952  acnnum  10037  alephord2i  10062  cardaleph  10074  aceq3lem  10105  dfac5lem5  10112  dfac12lem3  10130  ackbij1lem16  10218  cfslb  10251  cfslb2n  10253  cfsmolem  10255  fin4i  10283  infpssr  10293  fin1a2lem6  10390  axdc3lem2  10436  axcclem  10442  ttukeylem6  10499  fodomb  10511  gchi  10610  pwfseq  10650  inawina  10676  wunfi  10707  inar1  10761  ltexnq  10961  ltbtwnnq  10964  ltexprlem4  11025  ltexpri  11029  prlem936  11033  suplem1pr  11038  suplem2pr  11039  recexsrlem  11089  mulgt0sr  11091  map2psrpr  11096  supsr  11098  eqlei  11321  eqlei2  11322  ledivp1i  12141  nnind  12252  nnmulcl  12258  nn0ge2m1nn  12575  nnnegz  12595  ublbneg  12958  xmulasslem  13312  ixxssixx  13387  iccshftri  13515  iccshftli  13517  iccdili  13519  icccntri  13521  elfz1b  13623  fzo1fzo0n0  13746  elfzonlteqm1  13772  elfzo0l  13787  ssfzo12  13790  fzoopth  13793  elfzo1elm1fzo0  13799  elfzr  13812  elfzlmr  13813  zmodidfzoimp  13936  mptnn0fsuppr  14037  seqp1  14054  seqcl2  14058  seqfveq2  14062  seqshft2  14066  monoord  14070  seqsplit  14073  seqcaopr3  14075  seqf1olem2a  14078  seqf1o  14081  seqid2  14086  seqhomo  14087  hashf1rn  14390  hashinfxadd  14423  hashf1lem2  14495  seqcoll  14503  hash2pr  14508  pr2pwpr  14518  hashge2el2difr  14520  hash3tr  14530  fi1uzind  14546  brfi1indALT  14549  elovmptnn0wrd  14598  swrdswrd  14744  pfxccatin12lem2a  14766  swrdccat  14774  swrdccatin1d  14782  swrdccatin2d  14783  repswccat  14825  cshwidxmod  14842  relexpsucnnr  15064  rtrclreclem3  15099  rtrclreclem4  15100  dfrtrcl2  15101  relexpindlem  15102  relexpind  15103  rtrclind  15104  cjre  15192  climeu  15608  climub  15715  fsum2d  15824  fsumabs  15855  fsumrlim  15865  fsumo1  15866  fsumiun  15875  prodfn0  15950  prodfrec  15951  ntrivcvg  15953  fprodabs  16030  fprod2d  16037  fprodefsum  16150  ruclem9  16295  dvdsmod0  16317  p1modz1  16318  dvdsmodexp  16319  dvdsabseq  16372  mod2eq1n2dvds  16406  mulsucdiv2z  16412  nno  16441  nn0o  16442  sadcadd  16517  sadadd2  16519  saddisjlem  16523  smuval2  16541  smupval  16547  smueqlem  16549  smumullem  16551  dfgcd2  16605  lcmgcdlem  16665  lcmftp  16695  exprmfct  16764  eulerthlem2  16842  dvdsprmpweqnn  16946  dvdsprmpweqle  16947  pcmpt  16953  vdwlem10  17051  cshwsidrepsw  17154  cshwshashlem1  17156  prmlem1a  17167  setsn0fun  17234  ressval3d  17307  mreexexd  17705  letsr  18650  insubm  18878  ghmghmrn  19306  pmtrfrn  19529  pmtr3ncom  19546  gsmtrcl  19587  psgnsn  19591  sylow1lem1  19669  efginvrel2  19798  efgsrel  19805  cntzcmnss  19912  gsum2dlem2  20042  telgsumfzs  20060  dprdval  20076  ablfac1eulem  20145  pgpfac1  20153  pgpfac  20157  srgpcomp  20301  ringrng  20369  ring1ne0  20383  rngimf1o  20537  rngimrnghm  20538  rngimcnv  20539  0ringnnzr  20610  zrhpsgnelbas  21725  psgndiflemA  21732  mplcoe1  22169  mplcoe3  22170  mplcoe5lem  22171  mplcoe5  22172  mpfaddcl  22245  mpfmulcl  22246  coe1ae0  22357  coe1fzgsumd  22445  gsummoncoe1  22449  pf1addcl  22494  pf1mulcl  22495  evl1gsumd  22498  mamufacex  22534  mat0dimcrng  22608  mavmulsolcl  22689  mdetunilem9  22758  cramerlem3  22827  pmatcollpw3fi1  22926  pm2mpfo  22952  chmaidscmat  22986  chfacfscmul0  22996  chfacfpmmul0  23000  cpmadugsumlemF  23014  tg2  23103  neindisj2  23261  neiptopnei  23270  t1t0  23486  fiuncmp  23542  hmeof1o  23902  ist1-5lem  23958  t1r0  23959  alexsublem  24182  imasdsf1olem  24511  tgioo  24934  fsumcn  25010  voliunlem3  25692  itgfsum  25967  dvbsss  26042  dvmptfsum  26115  dvfsumlem2  26167  dvfsumlem4  26169  plyco  26379  dgrcolem1  26411  dgrco  26413  dvntaylp  26512  taylthlem1  26514  jensen  27131  bposlem5  27430  lgsqrmodndvds  27495  gausslemma2dlem0i  27506  gausslemma2dlem4  27511  lgsquad2lem2  27527  2lgslem3  27546  2lgs  27549  2lgsoddprm  27558  dchrisum0flb  27652  pntpbnd1  27728  pntlemf  27747  madebdayim  28059  oldbdayim  28060  pw2cut  28631  brbtwn  29227  brcgr  29228  umgrnloopv  29434  umgrnloop  29436  usgrnloopvALT  29529  usgrnloopALT  29531  usgredg2vlem2  29554  subgrprop  29601  uvtxnbgrvtx  29721  cusgrsize2inds  29781  rgrprop  29888  rusgrprop  29890  wlkprop  29939  wlkvtxeledg  29951  wlkeq  29961  wlkl1loop  29965  wlk1walk  29966  uspgr2wlkeqi  29975  wlkreslem  29995  wlkres  29996  redwlk  29998  lfgrwlknloop  30015  2pthnloop  30058  usgr2trlncl  30087  usgr2pth  30091  clwlkcompim  30107  clwlkcompbp  30109  uspgrn2crct  30135  crctcshwlkn0  30148  wwlknp  30170  wwlkswwlksn  30192  wlkiswwlks2lem4  30199  wlkiswwlks2  30202  wlklnwwlkln2lem  30209  wwlksnext  30220  wwlksnextbi  30221  wwlksnredwwlkn0  30223  wwlksnextwrd  30224  clwlkclwwlklem2a  30327  clwlkclwwlklem2  30329  clwlkclwwlkflem  30333  clwwisshclwws  30344  clwwlknp  30366  clwwlknwwlksn  30367  clwwlkwwlksb  30383  clwwlkext2edg  30385  umgrhashecclwwlk  30407  clwwlknun  30441  1pthond  30473  upgr3v3e3cycl  30509  upgr4cycl4dv4e  30514  eupth2  30568  3vfriswmgr  30607  3cyclfrgrrn1  30614  n4cyclfrgr  30620  frgrnbnb  30622  frgrncvvdeqlem3  30630  frgrncvvdeqlem6  30633  frgrncvvdeqlem7  30634  frgrncvvdeqlem8  30635  frgrwopreglem4a  30639  frgrwopreg  30652  frgrregorufr0  30653  frgr2wwlkeqm  30660  2clwwlk2clwwlklem  30675  wlkl0  30696  frgrreggt1  30722  frgrregord013  30724  frgrregord13  30725  frgrogt3nreg  30726  friendshipgt3  30727  friendship  30728  blocn2  31138  cvexchlem  32698  cdj3lem2b  32767  nnindf  33142  gsumwun  33374  domnprodn0  33576  issgon  34491  sitgclg  34710  sseqp1  34763  bnj938  35303  bnj964  35309  bnj1052  35341  bnj1125  35358  onvf1odlem4  35568  subfacp1lem6  35655  cvmliftlem7  35761  cvmliftlem10  35764  mclsrcl  36031  pprodss4v  36352  segleantisym  36585  rankeq1o  36641  bj-restv  37715  iooelexlt  37986  relowlssretop  37987  rdgeqoa  37994  matunitlindflem1  38245  poimirlem22  38271  poimirlem25  38274  poimirlem28  38277  poimirlem31  38280  mblfinlem3  38288  mbfresfi  38295  mettrifi  38386  opidon2OLD  38483  isexid2  38484  grpomndo  38504  elghomlem2OLD  38515  rngoidmlem  38565  rngoueqz  38569  iscringd  38627  cdlemk35s  41689  cdlemk39s  41691  cdlemk42  41693  uzindd  42723  mzpadd  43449  mzpmul  43450  mzpcompact2  43463  dford3lem2  43734  aomclem6  43766  cnsrexpcl  43872  ensucne0OLD  44236  pr2cv  44254  relexpss1d  44411  iunrelexpmin1  44414  iunrelexpmin2  44418  tfindsd  44914  nzin  45008  axc11next  45096  iotavalsb  45123  ssdec  45786  fperiodmullem  46002  monoordxrv  46175  fmul01  46276  fmulcl  46277  fmuldfeqlem1  46278  fmuldfeq  46279  iblspltprt  46667  itgspltprt  46673  stoweidlem2  46696  stoweidlem3  46697  stoweidlem6  46700  stoweidlem8  46702  stoweidlem17  46711  stoweidlem19  46713  stoweidlem21  46715  stoweidlem26  46720  stoweidlem31  46725  stoweidlem43  46737  fourierdlem42  46843  funressnfv  47757  eu2ndop1stv  47839  afv0fv0  47863  afv0nbfvbi  47865  funressnbrafv2  47958  funbrafv2  47961  nelbrim  47989  ssfz12  48028  smonoord  48091  iccpartiltu  48148  iccpartigtl  48149  iccelpart  48159  icceuelpart  48162  fargshiftf  48166  fargshiftf1  48167  fargshiftfo  48168  sprel  48210  sprsymrelf1lem  48217  sprsymrelfolem2  48219  prproropf1olem4  48232  lighneallem4  48339  mogoldbblem  48462  fpprnn  48472  fpprwppr  48481  fpprwpprb  48482  sbgoldbwt  48519  bgoldbtbndlem2  48548  bgoldbtbndlem4  48550  tgoldbach  48559  grimprop  48625  grlimprop  48726  grilcbri2  48753  upwlkwlk  48881  clcllaw  48933  intop  48945  clintop  48950  assintop  48951  assintopcllaw  48954  lmod0rng  48971  ztprmneprm  49104  scmsuppss  49128  ply1mulgsumlem1  49143  ply1mulgsumlem2  49144  lcoel0  49185  ellcoellss  49192  lindslinindsimp2lem5  49219  ldepspr  49230  flnn0div2ge  49290  nnolog2flm1  49347  blengt1fldiv2p1  49350  dignn0flhalf  49375  naryfvalelfv  49389  0aryfvalelfv  49392  fv1arycl  49394  fv2arycl  49405