Theorem mpcom 38

Description: Modus ponens inference with commutation of antecedents. Commuted form of mpd 15. (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:  anabsi5  669  axc16i  2438  mo4  2563  sbcn1  3846  sbcim1  3847  sbcim1OLD  3848  sbcbi1  3852  sbcel21v  3863  sbccomlem  3877  csbie2df  4448  elimasni  6111  sotri  6149  unixpid  6305  f0rn0  6793  f1ocnv  6860  funbrfv  6957  elfvmptrab1w  7042  f1dom3el3dif  7288  oprabidw  7461  oprabid  7462  oprabv  7492  ndmovordi  7623  elovmporab  7678  elovmporab1w  7679  elovmporab1  7680  elovmpt3rab1  7692  limomss  7891  unielxp  8050  bropfvvvvlem  8114  f1o2ndf1  8145  smogt  8405  tfrlem1  8414  oawordeulem  8590  omass  8616  ecopovtrn  8858  mapfvd  8917  findcard2d  9204  ssfi  9211  f1domfi  9218  php  9244  phpOLD  9256  unxpdom  9286  findcard3  9315  findcard3OLD  9316  isfinite2  9331  fsuppimp  9405  fsuppunfi  9425  fsuppunbi  9426  fsuppres  9430  infsupprpr  9541  cantnfval2  9706  cantnfle  9708  cantnfp1lem3  9717  cantnflem1  9726  cnfcom  9737  rankr1ai  9835  rankonidlem  9865  rankxplim2  9917  oncard  9997  ficardom  9998  cardne  10002  acnnum  10089  alephord2i  10114  cardaleph  10126  aceq3lem  10157  dfac5lem5  10164  dfac12lem3  10183  ackbij1lem16  10271  cfslb  10303  cfslb2n  10305  cfsmolem  10307  fin4i  10335  infpssr  10345  fin1a2lem6  10442  axdc3lem2  10488  axcclem  10494  ttukeylem6  10551  fodomb  10563  gchi  10661  pwfseq  10701  inawina  10727  wunfi  10758  inar1  10812  ltexnq  11012  ltbtwnnq  11015  ltexprlem4  11076  ltexpri  11080  prlem936  11084  suplem1pr  11089  suplem2pr  11090  recexsrlem  11140  mulgt0sr  11142  map2psrpr  11147  supsr  11149  eqlei  11368  eqlei2  11369  ledivp1i  12190  nnind  12281  nnmulcl  12287  nn0ge2m1nn  12593  nnnegz  12613  ublbneg  12972  xmulasslem  13323  ixxssixx  13397  iccshftri  13523  iccshftli  13525  iccdili  13527  icccntri  13529  elfz1b  13629  fzo1fzo0n0  13750  elfzonlteqm1  13776  elfzo0l  13791  ssfzo12  13794  fzoopth  13797  elfzo1elm1fzo0  13803  elfzr  13815  elfzlmr  13816  zmodidfzoimp  13937  mptnn0fsuppr  14036  seqp1  14053  seqcl2  14057  seqfveq2  14061  seqshft2  14065  monoord  14069  seqsplit  14072  seqcaopr3  14074  seqf1olem2a  14077  seqf1o  14080  seqid2  14085  seqhomo  14086  hashf1rn  14387  hashinfxadd  14420  hashf1lem2  14491  seqcoll  14499  hash2pr  14504  pr2pwpr  14514  hashge2el2difr  14516  hash3tr  14526  fi1uzind  14542  brfi1indALT  14545  elovmptnn0wrd  14593  swrdswrd  14739  pfxccatin12lem2a  14761  swrdccat  14769  swrdccatin1d  14777  swrdccatin2d  14778  repswccat  14820  cshwidxmod  14837  relexpsucnnr  15060  rtrclreclem3  15095  rtrclreclem4  15096  dfrtrcl2  15097  relexpindlem  15098  relexpind  15099  rtrclind  15100  cjre  15174  climeu  15587  climub  15694  fsum2d  15803  fsumabs  15833  fsumrlim  15843  fsumo1  15844  fsumiun  15853  prodfn0  15926  prodfrec  15927  ntrivcvg  15929  fprodabs  16006  fprod2d  16013  fprodefsum  16127  ruclem9  16270  dvdsmod0  16292  p1modz1  16293  dvdsmodexp  16294  dvdsabseq  16346  mod2eq1n2dvds  16380  mulsucdiv2z  16386  nno  16415  nn0o  16416  sadcadd  16491  sadadd2  16493  saddisjlem  16497  smuval2  16515  smupval  16521  smueqlem  16523  smumullem  16525  dfgcd2  16579  lcmgcdlem  16639  lcmftp  16669  exprmfct  16737  eulerthlem2  16815  dvdsprmpweqnn  16918  dvdsprmpweqle  16919  pcmpt  16925  vdwlem10  17023  cshwsidrepsw  17127  cshwshashlem1  17129  prmlem1a  17140  setsn0fun  17206  ressval3d  17291  ressval3dOLD  17292  mreexexd  17692  letsr  18650  insubm  18843  ghmghmrn  19265  pmtrfrn  19490  pmtr3ncom  19507  gsmtrcl  19548  psgnsn  19552  sylow1lem1  19630  efginvrel2  19759  efgsrel  19766  cntzcmnss  19873  gsum2dlem2  20003  telgsumfzs  20021  dprdval  20037  ablfac1eulem  20106  pgpfac1  20114  pgpfac  20118  srgpcomp  20235  ringrng  20298  ring1ne0  20312  rngimf1o  20470  rngimrnghm  20471  rngimcnv  20472  0ringnnzr  20541  zrhpsgnelbas  21629  psgndiflemA  21636  mplcoe1  22072  mplcoe3  22073  mplcoe5lem  22074  mplcoe5  22075  mpfaddcl  22146  mpfmulcl  22147  coe1ae0  22233  coe1fzgsumd  22323  gsummoncoe1  22327  pf1addcl  22372  pf1mulcl  22373  evl1gsumd  22376  mamufacex  22415  mat0dimcrng  22491  mavmulsolcl  22572  mdetunilem9  22641  cramerlem3  22710  pmatcollpw3fi1  22809  pm2mpfo  22835  chmaidscmat  22869  chfacfscmul0  22879  chfacfpmmul0  22883  cpmadugsumlemF  22897  tg2  22987  neindisj2  23146  neiptopnei  23155  t1t0  23371  fiuncmp  23427  hmeof1o  23787  ist1-5lem  23843  t1r0  23844  alexsublem  24067  imasdsf1olem  24398  tgioo  24831  fsumcn  24907  voliunlem3  25600  itgfsum  25876  dvbsss  25951  dvmptfsum  26027  dvfsumlem2  26081  dvfsumlem2OLD  26082  dvfsumlem4  26084  plyco  26294  dgrcolem1  26327  dgrco  26329  dvntaylp  26427  taylthlem1  26429  jensen  27046  bposlem5  27346  lgsqrmodndvds  27411  gausslemma2dlem0i  27422  gausslemma2dlem4  27427  lgsquad2lem2  27443  2lgslem3  27462  2lgs  27465  2lgsoddprm  27474  dchrisum0flb  27568  pntpbnd1  27644  pntlemf  27663  madebdayim  27940  oldbdayim  27941  pw2cut  28434  brbtwn  28928  brcgr  28929  umgrnloopv  29137  umgrnloop  29139  usgrnloopvALT  29232  usgrnloopALT  29234  usgredg2vlem2  29257  subgrprop  29304  uvtxnbgrvtx  29424  cusgrsize2inds  29485  rgrprop  29592  rusgrprop  29594  wlkprop  29643  wlkvtxeledg  29656  wlkeq  29666  wlkl1loop  29670  wlk1walk  29671  uspgr2wlkeqi  29680  wlkreslem  29701  wlkres  29702  redwlk  29704  lfgrwlknloop  29721  2pthnloop  29763  usgr2trlncl  29792  usgr2pth  29796  clwlkcompim  29812  clwlkcompbp  29814  uspgrn2crct  29837  crctcshwlkn0  29850  wwlknp  29872  wwlkswwlksn  29894  wlkiswwlks2lem4  29901  wlkiswwlks2  29904  wlklnwwlkln2lem  29911  wwlksnext  29922  wwlksnextbi  29923  wwlksnredwwlkn0  29925  wwlksnextwrd  29926  clwlkclwwlklem2a  30026  clwlkclwwlklem2  30028  clwlkclwwlkflem  30032  clwwisshclwws  30043  clwwlknp  30065  clwwlknwwlksn  30066  clwwlkwwlksb  30082  clwwlkext2edg  30084  umgrhashecclwwlk  30106  clwwlknun  30140  1pthond  30172  upgr3v3e3cycl  30208  upgr4cycl4dv4e  30213  eupth2  30267  3vfriswmgr  30306  3cyclfrgrrn1  30313  n4cyclfrgr  30319  frgrnbnb  30321  frgrncvvdeqlem3  30329  frgrncvvdeqlem6  30332  frgrncvvdeqlem7  30333  frgrncvvdeqlem8  30334  frgrwopreglem4a  30338  frgrwopreg  30351  frgrregorufr0  30352  frgr2wwlkeqm  30359  2clwwlk2clwwlklem  30374  wlkl0  30395  frgrreggt1  30421  frgrregord013  30423  frgrregord13  30424  frgrogt3nreg  30425  friendshipgt3  30426  friendship  30427  blocn2  30836  cvexchlem  32396  cdj3lem2b  32465  cnvoprabOLD  32737  nnindf  32825  gsumwun  33050  domnprodn0  33261  issgon  34103  sitgclg  34323  sseqp1  34376  bnj938  34929  bnj964  34935  bnj1052  34967  bnj1125  34984  subfacp1lem6  35169  cvmliftlem7  35275  cvmliftlem10  35278  mclsrcl  35545  pprodss4v  35865  segleantisym  36096  rankeq1o  36152  bj-restv  37077  iooelexlt  37344  relowlssretop  37345  rdgeqoa  37352  matunitlindflem1  37602  poimirlem22  37628  poimirlem25  37631  poimirlem28  37634  poimirlem31  37637  mblfinlem3  37645  mbfresfi  37652  mettrifi  37743  opidon2OLD  37840  isexid2  37841  grpomndo  37861  elghomlem2OLD  37872  rngoidmlem  37922  rngoueqz  37926  iscringd  37984  cdlemk35s  40919  cdlemk39s  40921  cdlemk42  40923  uzindd  41958  mzpadd  42725  mzpmul  42726  mzpcompact2  42739  dford3lem2  43015  aomclem6  43047  cnsrexpcl  43153  ensucne0OLD  43519  pr2cv  43537  relexpss1d  43694  iunrelexpmin1  43697  iunrelexpmin2  43701  tfindsd  44200  nzin  44313  axc11next  44401  iotavalsb  44428  ssdec  45027  fperiodmullem  45253  monoordxrv  45431  fmul01  45535  fmulcl  45536  fmuldfeqlem1  45537  fmuldfeq  45538  iblspltprt  45928  itgspltprt  45934  stoweidlem2  45957  stoweidlem3  45958  stoweidlem6  45961  stoweidlem8  45963  stoweidlem17  45972  stoweidlem19  45974  stoweidlem21  45976  stoweidlem26  45981  stoweidlem31  45986  stoweidlem43  45998  fourierdlem42  46104  funressnfv  46992  eu2ndop1stv  47074  afv0fv0  47098  afv0nbfvbi  47100  funressnbrafv2  47193  funbrafv2  47196  nelbrim  47224  ssfz12  47263  smonoord  47295  iccpartiltu  47346  iccpartigtl  47347  iccelpart  47357  icceuelpart  47360  fargshiftf  47364  fargshiftf1  47365  fargshiftfo  47366  sprel  47408  sprsymrelf1lem  47415  sprsymrelfolem2  47417  prproropf1olem4  47430  lighneallem4  47534  mogoldbblem  47644  fpprnn  47654  fpprwppr  47663  fpprwpprb  47664  sbgoldbwt  47701  bgoldbtbndlem2  47730  bgoldbtbndlem4  47732  tgoldbach  47741  grimprop  47806  grlimprop  47886  grilcbri2  47906  upwlkwlk  47982  clcllaw  48034  intop  48046  clintop  48051  assintop  48052  assintopcllaw  48055  lmod0rng  48072  ztprmneprm  48191  scmsuppss  48215  ply1mulgsumlem1  48231  ply1mulgsumlem2  48232  lcoel0  48273  ellcoellss  48280  lindslinindsimp2lem5  48307  ldepspr  48318  flnn0div2ge  48382  nnolog2flm1  48439  blengt1fldiv2p1  48442  dignn0flhalf  48467  naryfvalelfv  48481  0aryfvalelfv  48484  fv1arycl  48486  fv2arycl  48497