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  2440  mo4  2565  sbcn1  3818  sbcim1  3819  sbcbi1  3823  sbcel21v  3833  sbccomlem  3844  csbie2df  4418  elimasni  6078  sotri  6116  unixpid  6273  f0rn0  6762  f1ocnv  6829  funbrfv  6926  elfvmptrab1w  7012  f1dom3el3dif  7261  oprabidw  7434  oprabid  7435  oprabv  7465  ndmovordi  7596  elovmporab  7651  elovmporab1w  7652  elovmporab1  7653  elovmpt3rab1  7665  limomss  7864  unielxp  8024  bropfvvvvlem  8088  f1o2ndf1  8119  smogt  8379  tfrlem1  8388  oawordeulem  8564  omass  8590  ecopovtrn  8832  mapfvd  8891  findcard2d  9178  ssfi  9185  f1domfi  9193  php  9219  phpOLD  9229  unxpdom  9259  findcard3  9288  findcard3OLD  9289  isfinite2  9304  fsuppimp  9378  fsuppunfi  9398  fsuppunbi  9399  fsuppres  9403  infsupprpr  9516  cantnfval2  9681  cantnfle  9683  cantnfp1lem3  9692  cantnflem1  9701  cnfcom  9712  rankr1ai  9810  rankonidlem  9840  rankxplim2  9892  oncard  9972  ficardom  9973  cardne  9977  acnnum  10064  alephord2i  10089  cardaleph  10101  aceq3lem  10132  dfac5lem5  10139  dfac12lem3  10158  ackbij1lem16  10246  cfslb  10278  cfslb2n  10280  cfsmolem  10282  fin4i  10310  infpssr  10320  fin1a2lem6  10417  axdc3lem2  10463  axcclem  10469  ttukeylem6  10526  fodomb  10538  gchi  10636  pwfseq  10676  inawina  10702  wunfi  10733  inar1  10787  ltexnq  10987  ltbtwnnq  10990  ltexprlem4  11051  ltexpri  11055  prlem936  11059  suplem1pr  11064  suplem2pr  11065  recexsrlem  11115  mulgt0sr  11117  map2psrpr  11122  supsr  11124  eqlei  11343  eqlei2  11344  ledivp1i  12165  nnind  12256  nnmulcl  12262  nn0ge2m1nn  12569  nnnegz  12589  ublbneg  12947  xmulasslem  13299  ixxssixx  13374  iccshftri  13502  iccshftli  13504  iccdili  13506  icccntri  13508  elfz1b  13608  fzo1fzo0n0  13729  elfzonlteqm1  13755  elfzo0l  13770  ssfzo12  13773  fzoopth  13776  elfzo1elm1fzo0  13782  elfzr  13794  elfzlmr  13795  zmodidfzoimp  13916  mptnn0fsuppr  14015  seqp1  14032  seqcl2  14036  seqfveq2  14040  seqshft2  14044  monoord  14048  seqsplit  14051  seqcaopr3  14053  seqf1olem2a  14056  seqf1o  14059  seqid2  14064  seqhomo  14065  hashf1rn  14368  hashinfxadd  14401  hashf1lem2  14472  seqcoll  14480  hash2pr  14485  pr2pwpr  14495  hashge2el2difr  14497  hash3tr  14507  fi1uzind  14523  brfi1indALT  14526  elovmptnn0wrd  14575  swrdswrd  14721  pfxccatin12lem2a  14743  swrdccat  14751  swrdccatin1d  14759  swrdccatin2d  14760  repswccat  14802  cshwidxmod  14819  relexpsucnnr  15042  rtrclreclem3  15077  rtrclreclem4  15078  dfrtrcl2  15079  relexpindlem  15080  relexpind  15081  rtrclind  15082  cjre  15156  climeu  15569  climub  15676  fsum2d  15785  fsumabs  15815  fsumrlim  15825  fsumo1  15826  fsumiun  15835  prodfn0  15908  prodfrec  15909  ntrivcvg  15911  fprodabs  15988  fprod2d  15995  fprodefsum  16109  ruclem9  16254  dvdsmod0  16276  p1modz1  16277  dvdsmodexp  16278  dvdsabseq  16330  mod2eq1n2dvds  16364  mulsucdiv2z  16370  nno  16399  nn0o  16400  sadcadd  16475  sadadd2  16477  saddisjlem  16481  smuval2  16499  smupval  16505  smueqlem  16507  smumullem  16509  dfgcd2  16563  lcmgcdlem  16623  lcmftp  16653  exprmfct  16721  eulerthlem2  16799  dvdsprmpweqnn  16903  dvdsprmpweqle  16904  pcmpt  16910  vdwlem10  17008  cshwsidrepsw  17111  cshwshashlem1  17113  prmlem1a  17124  setsn0fun  17190  ressval3d  17265  mreexexd  17658  letsr  18601  insubm  18794  ghmghmrn  19216  pmtrfrn  19437  pmtr3ncom  19454  gsmtrcl  19495  psgnsn  19499  sylow1lem1  19577  efginvrel2  19706  efgsrel  19713  cntzcmnss  19820  gsum2dlem2  19950  telgsumfzs  19968  dprdval  19984  ablfac1eulem  20053  pgpfac1  20061  pgpfac  20065  srgpcomp  20176  ringrng  20243  ring1ne0  20257  rngimf1o  20412  rngimrnghm  20413  rngimcnv  20414  0ringnnzr  20483  zrhpsgnelbas  21552  psgndiflemA  21559  mplcoe1  21993  mplcoe3  21994  mplcoe5lem  21995  mplcoe5  21996  mpfaddcl  22061  mpfmulcl  22062  coe1ae0  22150  coe1fzgsumd  22240  gsummoncoe1  22244  pf1addcl  22289  pf1mulcl  22290  evl1gsumd  22293  mamufacex  22332  mat0dimcrng  22406  mavmulsolcl  22487  mdetunilem9  22556  cramerlem3  22625  pmatcollpw3fi1  22724  pm2mpfo  22750  chmaidscmat  22784  chfacfscmul0  22794  chfacfpmmul0  22798  cpmadugsumlemF  22812  tg2  22901  neindisj2  23059  neiptopnei  23068  t1t0  23284  fiuncmp  23340  hmeof1o  23700  ist1-5lem  23756  t1r0  23757  alexsublem  23980  imasdsf1olem  24310  tgioo  24733  fsumcn  24810  voliunlem3  25503  itgfsum  25778  dvbsss  25853  dvmptfsum  25929  dvfsumlem2  25983  dvfsumlem2OLD  25984  dvfsumlem4  25986  plyco  26196  dgrcolem1  26229  dgrco  26231  dvntaylp  26329  taylthlem1  26331  jensen  26949  bposlem5  27249  lgsqrmodndvds  27314  gausslemma2dlem0i  27325  gausslemma2dlem4  27330  lgsquad2lem2  27346  2lgslem3  27365  2lgs  27368  2lgsoddprm  27377  dchrisum0flb  27471  pntpbnd1  27547  pntlemf  27566  madebdayim  27843  oldbdayim  27844  pw2cut  28337  brbtwn  28824  brcgr  28825  umgrnloopv  29031  umgrnloop  29033  usgrnloopvALT  29126  usgrnloopALT  29128  usgredg2vlem2  29151  subgrprop  29198  uvtxnbgrvtx  29318  cusgrsize2inds  29379  rgrprop  29486  rusgrprop  29488  wlkprop  29537  wlkvtxeledg  29550  wlkeq  29560  wlkl1loop  29564  wlk1walk  29565  uspgr2wlkeqi  29574  wlkreslem  29595  wlkres  29596  redwlk  29598  lfgrwlknloop  29615  2pthnloop  29659  usgr2trlncl  29688  usgr2pth  29692  clwlkcompim  29708  clwlkcompbp  29710  uspgrn2crct  29736  crctcshwlkn0  29749  wwlknp  29771  wwlkswwlksn  29793  wlkiswwlks2lem4  29800  wlkiswwlks2  29803  wlklnwwlkln2lem  29810  wwlksnext  29821  wwlksnextbi  29822  wwlksnredwwlkn0  29824  wwlksnextwrd  29825  clwlkclwwlklem2a  29925  clwlkclwwlklem2  29927  clwlkclwwlkflem  29931  clwwisshclwws  29942  clwwlknp  29964  clwwlknwwlksn  29965  clwwlkwwlksb  29981  clwwlkext2edg  29983  umgrhashecclwwlk  30005  clwwlknun  30039  1pthond  30071  upgr3v3e3cycl  30107  upgr4cycl4dv4e  30112  eupth2  30166  3vfriswmgr  30205  3cyclfrgrrn1  30212  n4cyclfrgr  30218  frgrnbnb  30220  frgrncvvdeqlem3  30228  frgrncvvdeqlem6  30231  frgrncvvdeqlem7  30232  frgrncvvdeqlem8  30233  frgrwopreglem4a  30237  frgrwopreg  30250  frgrregorufr0  30251  frgr2wwlkeqm  30258  2clwwlk2clwwlklem  30273  wlkl0  30294  frgrreggt1  30320  frgrregord013  30322  frgrregord13  30323  frgrogt3nreg  30324  friendshipgt3  30325  friendship  30326  blocn2  30735  cvexchlem  32295  cdj3lem2b  32364  nnindf  32744  gsumwun  33005  domnprodn0  33216  issgon  34100  sitgclg  34320  sseqp1  34373  bnj938  34914  bnj964  34920  bnj1052  34952  bnj1125  34969  subfacp1lem6  35153  cvmliftlem7  35259  cvmliftlem10  35262  mclsrcl  35529  pprodss4v  35848  segleantisym  36079  rankeq1o  36135  bj-restv  37059  iooelexlt  37326  relowlssretop  37327  rdgeqoa  37334  matunitlindflem1  37586  poimirlem22  37612  poimirlem25  37615  poimirlem28  37618  poimirlem31  37621  mblfinlem3  37629  mbfresfi  37636  mettrifi  37727  opidon2OLD  37824  isexid2  37825  grpomndo  37845  elghomlem2OLD  37856  rngoidmlem  37906  rngoueqz  37910  iscringd  37968  cdlemk35s  40902  cdlemk39s  40904  cdlemk42  40906  uzindd  41936  mzpadd  42708  mzpmul  42709  mzpcompact2  42722  dford3lem2  42998  aomclem6  43030  cnsrexpcl  43136  ensucne0OLD  43501  pr2cv  43519  relexpss1d  43676  iunrelexpmin1  43679  iunrelexpmin2  43683  tfindsd  44182  nzin  44290  axc11next  44378  iotavalsb  44405  ssdec  45060  fperiodmullem  45280  monoordxrv  45456  fmul01  45557  fmulcl  45558  fmuldfeqlem1  45559  fmuldfeq  45560  iblspltprt  45950  itgspltprt  45956  stoweidlem2  45979  stoweidlem3  45980  stoweidlem6  45983  stoweidlem8  45985  stoweidlem17  45994  stoweidlem19  45996  stoweidlem21  45998  stoweidlem26  46003  stoweidlem31  46008  stoweidlem43  46020  fourierdlem42  46126  funressnfv  47020  eu2ndop1stv  47102  afv0fv0  47126  afv0nbfvbi  47128  funressnbrafv2  47221  funbrafv2  47224  nelbrim  47252  ssfz12  47291  smonoord  47333  iccpartiltu  47384  iccpartigtl  47385  iccelpart  47395  icceuelpart  47398  fargshiftf  47402  fargshiftf1  47403  fargshiftfo  47404  sprel  47446  sprsymrelf1lem  47453  sprsymrelfolem2  47455  prproropf1olem4  47468  lighneallem4  47572  mogoldbblem  47682  fpprnn  47692  fpprwppr  47701  fpprwpprb  47702  sbgoldbwt  47739  bgoldbtbndlem2  47768  bgoldbtbndlem4  47770  tgoldbach  47779  grimprop  47844  grlimprop  47944  grilcbri2  47964  upwlkwlk  48062  clcllaw  48114  intop  48126  clintop  48131  assintop  48132  assintopcllaw  48135  lmod0rng  48152  ztprmneprm  48270  scmsuppss  48294  ply1mulgsumlem1  48310  ply1mulgsumlem2  48311  lcoel0  48352  ellcoellss  48359  lindslinindsimp2lem5  48386  ldepspr  48397  flnn0div2ge  48461  nnolog2flm1  48518  blengt1fldiv2p1  48521  dignn0flhalf  48546  naryfvalelfv  48560  0aryfvalelfv  48563  fv1arycl  48565  fv2arycl  48576