MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  expcom Structured version   Visualization version   GIF version

Theorem expcom 450
Description: Exportation inference with commuted antecedents. (Contributed by NM, 25-May-2005.)
Hypothesis
Ref Expression
ex.1 ((𝜑𝜓) → 𝜒)
Assertion
Ref Expression
expcom (𝜓 → (𝜑𝜒))

Proof of Theorem expcom
StepHypRef Expression
1 ex.1 . . 3 ((𝜑𝜓) → 𝜒)
21ex 449 . 2 (𝜑 → (𝜓𝜒))
32com12 32 1 (𝜓 → (𝜑𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 197  df-an 385
This theorem is referenced by:  ancoms  468  syldan  488  sylan  489  4casesdan  1028  dedlema  1032  dedlemb  1033  cbval2  2425  cbvaldva  2427  2moswap  2686  2eu2  2693  pm2.61ne  3018  nelelne  3031  r19.21be  3072  rspcebdv  3455  minel  4178  uneqdifeq  4202  uneqdifeqOLD  4203  raltpd  4459  ssunsn2  4505  opthprneg  4546  ssuni  4612  ssuniOLD  4613  uniss2  4623  elpwuni  4769  disjord  4794  elssabg  4969  elpw2g  4977  oteqex  5113  otsndisj  5130  otiunsndisj  5131  epelg  5181  wereu  5263  relop  5429  riinint  5538  sotri3  5685  unixpid  5832  ordtr2  5930  ordsssuc2  5976  funopg  6084  fun  6228  tz6.12c  6376  fvmptnf  6466  fvn0ssdmfun  6515  eldmrexrnb  6531  fmptco  6561  funopsn  6578  fnressn  6590  fressnfv  6592  fvtp2g  6630  fvtp3g  6631  fconst2g  6634  fntpb  6639  f1dom3el3dif  6691  isores3  6750  isoselem  6756  oprabv  6870  eloprabga  6914  sorpsscmpl  7115  difex2  7136  ordpwsuc  7182  ordsucun  7192  limuni3  7219  ordom  7241  fo1stres  7361  poxp  7459  soxp  7460  suppimacnv  7476  frnsuppeq  7477  funsssuppss  7492  brtpos2  7529  wfrlem12  7597  onnseq  7612  smores  7620  smofvon2  7624  tfrlem1  7643  oacl  7787  omcl  7788  oecl  7789  oawordri  7802  oalimcl  7812  oaass  7813  oarec  7814  omwordri  7824  omeulem1  7834  omeulem2  7835  oeordi  7839  oeworde  7845  oeoelem  7850  nnacl  7863  nnmcl  7864  nnecl  7865  nnacom  7869  nnaass  7874  nnmsucr  7877  nnmordi  7883  omabs  7899  iiner  7989  elpmg  8042  pmss12g  8053  mapsn  8068  f1domg  8144  ssdomg  8170  domtriord  8274  php  8312  php3  8314  1sdom  8331  fisseneq  8339  isinf  8341  ssnnfi  8347  dif1en  8361  findcard3  8371  frfi  8373  unfi  8395  difinf  8398  fnfi  8406  iunfi  8422  fsuppunfi  8463  fsuppres  8468  frnfsuppbi  8472  elfi2  8488  marypha1lem  8507  marypha1  8508  oiexg  8608  wemapso2  8626  harword  8638  brwdom  8640  unxpwdom  8662  en3lplem1  8683  inf3lemd  8700  inf3lem5  8705  cantnfval2  8742  cantnfle  8744  cantnflt  8745  cnfcom  8773  tcmin  8793  r1sdom  8813  rankxplim3  8920  cardidm  8996  cardmin2  9035  infxpenlem  9047  fseqenlem1  9058  numacn  9083  alephordi  9108  iscard3  9127  alephinit  9129  carduniima  9130  iunfictbso  9148  dfac5  9162  dfac12lem3  9180  pwsdompw  9239  pwcdadom  9251  cflim2  9298  cfslb2n  9303  cofsmo  9304  cfsmolem  9305  cfcoflem  9307  alephsing  9311  infpssALT  9348  fin23lem34  9381  isf32lem2  9389  isf32lem10  9397  isf32lem12  9399  isfin1-2  9420  hsmexlem4  9464  axcc2lem  9471  domtriomlem  9477  axdc2lem  9483  axdc3lem2  9486  axdc3lem4  9488  axdc4lem  9490  axcclem  9492  ac6num  9514  ac6s  9519  zorn2lem7  9537  ttukeylem5  9548  imadomg  9569  iundom2g  9575  ondomon  9598  ficard  9600  konigthlem  9603  alephreg  9617  pwcfsdom  9618  cfpwsdom  9619  axregndlem1  9637  axregnd  9639  pwfseqlem3  9695  pwxpndom2  9700  pwxpndom  9701  pwcdandom  9702  inawinalem  9724  gchina  9734  wuncval2  9782  tsk0  9798  tskxpss  9807  inatsk  9813  tskuni  9818  gruina  9853  grothac  9865  addclpi  9927  addnidpi  9936  nqereu  9964  mulcanenq  9995  genpnnp  10040  nqpr  10049  prlem934  10068  reclem2pr  10083  suplem1pr  10087  supsrlem  10145  axpre-sup  10203  1re  10252  dedekindle  10414  00id  10424  receu  10885  sup3  11193  infrelb  11221  peano5nni  11236  nnaddcl  11255  zrevaddcl  11635  nzadd  11638  zdiv  11660  nneo  11674  zeo2  11677  nn0indd  11687  fzind  11688  fnn0ind  11689  uzwo  11965  lbzbi  11990  nn01to3  11995  qrevaddcl  12024  irradd  12026  irrmul  12027  ltsubrp  12080  ltaddrp  12081  xnn0xaddcl  12280  xnn0xadd0  12291  icoshft  12508  fzen  12572  elfzm11  12625  uzsplit  12626  elfzoext  12740  elfzom1elp1fzo  12750  injresinjlem  12803  injresinj  12804  modifeq2int  12947  modsumfzodifsn  12958  om2uzlti  12964  ssnn0fi  12999  fsuppmapnn0fiub0  13008  mptnn0fsuppr  13014  seqcl2  13034  seqfveq2  13038  seqshft2  13042  monoord  13046  seqsplit  13049  seqcaopr3  13051  seqf1olem2a  13054  seqf1o  13057  seqid2  13062  seqhomo  13063  ser1const  13072  expadd  13117  expmul  13120  leexp1a  13134  faccl  13285  facdiv  13289  faclbnd  13292  faclbnd4lem4  13298  faclbnd6  13301  hasheqf1oi  13355  hashgadd  13379  hashinfxadd  13387  hashunx  13388  hashunsng  13394  elprchashprn2  13397  hashss  13410  hash1snb  13420  hashmap  13435  hashf1lem2  13453  hashf1  13454  seqcoll  13461  hashle2pr  13472  hashdmpropge2  13478  hashge3el3dif  13481  hash1to3  13486  fundmge2nop0  13487  fi1uzind  13492  brfi1indALT  13495  sswrd  13520  swrdnd2  13654  swrdswrdlem  13680  swrdswrd  13681  wrd2ind  13698  swrdccatin1  13704  swrdccatin2  13708  swrdccatin12lem2  13710  swrdccat3  13713  repsdf2  13746  repswswrd  13752  cshw0  13761  cshwcl  13765  cshwlen  13766  cshf1  13777  swrdco  13804  relexpsucnnl  13992  rtrclreclem3  14020  rtrclreclem4  14021  relexpindlem  14023  rtrclind  14025  shftlem  14028  caubnd  14318  rlimcld2  14529  o1dif  14580  climub  14612  climserle  14613  iseraltlem2  14633  sumss  14675  fsumzcl2  14689  fsummsnunz  14703  fsumsplitsnun  14704  fsummsnunzOLD  14705  fsumsplitsnunOLD  14706  fsum2d  14722  modfsummods  14745  fsumabs  14753  fsumrlim  14763  fsumo1  14764  fsumiun  14773  bcxmas  14787  climcndslem1  14801  climcndslem2  14802  cvgrat  14835  clim2prod  14840  prodfn0  14846  prodfrec  14847  ntrivcvg  14849  prodmo  14886  fprodss  14898  fprodabs  14924  fprodn0  14929  fprod2d  14931  fprodefsum  15045  ruclem8  15186  ruclem9  15187  dvdsmod0  15209  dvds2ln  15237  dvdsaddre2b  15252  dvdslelem  15254  dvdsdivcl  15261  alzdvds  15265  mod2eq1n2dvds  15294  oddnn02np1  15295  nn0o1gt2  15320  nno  15321  sumeven  15333  sumodd  15334  pwp1fsum  15337  ndvdsadd  15357  bitsinv1  15387  sadcadd  15403  sadadd2  15405  saddisjlem  15409  smuval2  15427  smupvallem  15428  smu01lem  15430  smupval  15433  smueqlem  15435  smumullem  15437  gcddiv  15491  gcdmultiple  15492  rplpwr  15499  nn0seqcvgd  15506  seq1st  15507  alginv  15511  algcvga  15515  algfx  15516  absprodnn  15554  isprm2  15618  isprm3  15619  prmind2  15621  maxprmfct  15644  prmdvdsexp  15650  pcmpt  15819  prmreclem4  15846  vdwmc2  15906  vdwlem10  15917  ramub2  15941  ramcl  15956  prmgaplem5  15982  prmgaplem8  15985  cshwshashlem1  16025  cshwshashlem3  16027  setsn0fun  16118  imasleval  16424  divsfval  16430  mreexexlem4d  16530  isssc  16702  initoeu1  16883  termoeu1  16890  istos  17257  mgmcl  17467  frmdgsum  17621  dfgrp3lem  17735  mhmmulg  17805  resghm2b  17900  gsumwrev  18017  elsymgbas  18023  symgextf1  18062  gsmsymgreqlem2  18072  gsmsymgreq  18073  odlem1  18175  odcl2  18203  gexlem1  18215  sylow1lem1  18234  efgi2  18359  efginvrel2  18361  efgsrel  18368  cyggexb  18521  gsummulglem  18562  gsumzunsnd  18576  gsum2dlem2  18591  telgsums  18611  dmdprd  18618  dprdw  18630  ablfac1eulem  18692  srgpcomp  18753  lmodfopnelem1  19122  rmodislmodlem  19153  mplcoe1  19688  mplcoe3  19689  mplcoe5  19691  cply1mul  19887  coe1fzgsumdlem  19894  gsummoncoe1  19897  pf1ind  19942  evl1gsumdlem  19943  cnfldmulg  20001  cnfldexp  20002  obslbs  20297  mat1dimcrng  20506  ma1repveval  20600  mulmarep1gsum2  20603  gsummatr01lem3  20686  cramerlem3  20718  decpmatmulsumfsupp  20801  mp2pm2mplem4  20837  pm2mpmhmlem1  20846  fvmptnn04if  20877  cayhamlem1  20894  fctop  21031  mretopd  21119  restopnb  21202  restdis  21205  tgcnp  21280  cncls2  21300  cncls  21301  cnntr  21302  cnsscnp  21306  cmpsub  21426  2ndcsep  21485  1stcelcls  21487  lfinpfin  21550  locfincmp  21552  comppfsc  21558  txcn  21652  txlm  21674  xkohaus  21679  qtopres  21724  haushmphlem  21813  cmphmph  21814  connhmph  21815  reghmph  21819  nrmhmph  21820  ptcmpfi  21839  reghaus  21851  fbssfi  21863  fbun  21866  fbfinnfr  21867  isfildlem  21883  fgcl  21904  cfinfil  21919  supfil  21921  ufinffr  21955  fin1aufil  21958  cnpflf  22027  alexsubALTlem3  22075  alexsubALT  22077  cnextfvval  22091  cnextcn  22093  tmdmulg  22118  tmdgsum  22121  tgphaus  22142  tgpt1  22143  mettri  22379  imasdsf1olem  22400  blssexps  22453  blssex  22454  mopni3  22521  metss  22535  psmetutop  22594  dscmet  22599  tngngp3  22682  rectbntr0  22857  metnrmlem1a  22883  fsumcn  22895  lmmbr  23277  caubl  23327  caublcls  23328  bcthlem5  23346  bcth3  23349  ovolunlem1a  23485  ovoliunnul  23496  ovolicc2lem3  23508  finiunmbl  23533  voliunlem1  23539  volsuplem  23544  volsup  23545  dyadmax  23587  itgfsum  23813  dvnadd  23912  dvnres  23914  cpnord  23918  dvnfre  23935  dvmptfsum  23958  dvlip  23976  fta1g  24147  plyco  24217  dgrcolem1  24249  dgrco  24251  dvnply2  24262  plydivex  24272  plyexmo  24288  aannenlem1  24303  aaliou3lem2  24318  dvntaylp  24345  taylthlem1  24347  ulmval  24354  cxpmul2  24656  scvxcvx  24933  jensenlem2  24935  jensen  24936  ppiub  25150  bcmono  25223  bpos1lem  25228  bposlem5  25234  gausslemma2dlem6  25318  lgsquad2lem2  25331  2lgslem3  25350  2lgs  25353  dchrisumlem1  25399  dchrisum0flb  25420  pntpbnd1  25496  pntlemf  25515  qabvle  25535  qabvexp  25536  ostthlem2  25538  ostth2lem2  25544  axeuclidlem  26063  axcontlem12  26076  umgrnloopv  26222  uhgredgrnv  26246  edglnl  26259  numedglnl  26260  usgruspgrb  26297  usgrnloopvALT  26314  usgredg2vlem2  26339  subupgr  26400  nbumgr  26464  uhgrnbgr0nb  26471  nbgr0vtxlem  26472  edgusgrnbfin  26495  nb3grprlem2  26503  uvtxnbgrvtx  26517  cplgrop  26565  cusgrfi  26586  fusgrmaxsize  26592  fusgrn0degnn0  26627  ewlkprop  26731  uspgr2wlkeq  26774  g0wlk0  26780  wlkreslem  26798  wlkres  26799  lfgriswlk  26817  upgrwlkdvde  26865  spthonepeq  26880  uhgrwkspth  26883  usgr2trlncl  26888  usgr2trlspth  26889  cyclnspth  26928  crctcshwlkn0lem3  26937  wwlksn  26962  wspthneq1eq2  26991  wwlksm1edg  27012  wwlksnred  27032  wwlksnextfun  27038  wwlksnextinj  27039  wwlksnextproplem3  27051  wspthsnonn0vne  27059  wspn0  27066  rusgrnumwwlk  27119  clwwlkccatlem  27134  umgrclwwlkge2  27136  clwlkclwwlklem2  27145  clwlkclwwlklem3  27146  clwwisshclwws  27160  clwwisshclwwsn  27161  clwwlknOLD  27174  clwwlkn1loopb  27194  clwwlknfi  27196  wwlksext2clwwlk  27209  wwlksubclwwlk  27211  clwlksfclwwlkOLD  27238  clwwlknonwwlknonb  27276  clwwlknonex2lem2  27279  upgr3v3e3cycl  27354  uhgr3cyclex  27356  upgr4cycl4dv4e  27359  eupthseg  27380  upgreupthseg  27383  eupth2lem3lem4  27405  eupth2lem3lem7  27408  eupth2  27413  eulerpath  27415  nfrgr2v  27448  frgr3vlem1  27449  3vfriswmgr  27454  1to2vfriswmgr  27455  1to3vfriswmgr  27456  3cyclfrgrrn1  27461  3cyclfrgrrn  27462  3cyclfrgrrn2  27463  4cycl2vnunb  27466  frgrncvvdeqlem2  27476  frgrncvvdeqlem8  27482  frgrncvvdeqlem9  27483  frgrwopreglem4a  27486  frgrwopreglem5lem  27496  frgrwopreglem5ALT  27498  frgrregorufr0  27500  frgr2wwlk1  27505  frgr2wwlkeqm  27507  fusgr2wsp2nb  27510  2wspmdisj  27513  frrusgrord  27517  numclwlk1lem2f1  27538  numclwlk1  27554  frgrreggt1  27583  friendshipgt3  27588  hlim2  28380  elnlfn  29118  stle0i  29429  hstrbi  29456  spansncv2  29483  h1da  29539  fmptcof2  29788  nnindd  29897  xreceu  29961  tpr2rico  30289  hasheuni  30478  ismeas  30593  sseqp1  30788  rrvsum  30847  dstfrvunirn  30867  sgn3da  30934  bnj607  31315  bnj1145  31390  bnj1204  31409  subfacp1lem6  31496  cvmliftlem7  31602  cvmliftlem10  31605  cvmlift2lem12  31625  cvmlift3lem4  31633  mrsubvrs  31748  climuzcnv  31894  iprodefisumlem  31955  fprb  31998  dfon2lem9  32023  trpredtr  32057  trpredmintr  32058  dftrpred3g  32060  trpredrec  32065  soseq  32082  sltval2  32137  sltsolem1  32154  linethru  32588  elhf2  32610  finminlem  32640  fnessref  32680  neibastop2lem  32683  fnemeet2  32690  nndivsub  32784  bj-cbval2v  33066  bj-xpnzex  33271  bj-intss  33378  mptsnunlem  33515  dissneqlem  33517  topdifinffinlem  33525  iooelexlt  33540  wl-exeq  33653  wl-ax11-lem3  33696  matunitlindflem1  33737  poimirlem22  33763  poimirlem26  33767  poimirlem28  33769  poimirlem29  33770  poimirlem32  33773  heicant  33776  ovoliunnfl  33783  voliunnfl  33785  volsupnfl  33786  cover2  33840  upixp  33856  sdclem2  33870  fdc  33873  seqpo  33875  metf1o  33883  mettrifi  33885  sstotbnd3  33907  heibor1lem  33940  heiborlem5  33946  heibor  33952  bfplem1  33953  elghomlem2OLD  34017  grpokerinj  34024  isrngo  34028  rngodm1dm2  34063  ispridl2  34169  exlimddvf  34258  lssatle  34824  4atexlemex4  35881  mzpsubst  37832  jm2.18  38076  wepwsolem  38133  iunrelexp0  38515  relexpmulg  38523  cnvtrclfv  38537  clsk1indlem3  38862  dvgrat  39032  radcnvrat  39034  sbcoreleleqVD  39613  csbxpgVD  39648  sineq0ALT  39691  monoordxrv  40229  islptre  40373  iblspltprt  40711  stoweidlem2  40741  stoweidlem17  40756  stoweidlem21  40760  2reu2  41712  afveu  41758  funbrafv  41763  ndmaovass  41811  funop1  41829  fvmptrabdm  41836  nltle2tri  41852  2elfz2melfz  41857  fzoopth  41866  smonoord  41870  fsummsndifre  41871  fsumsplitsndif  41872  fsummmodsndifre  41873  fsummmodsnunz  41874  iccpartimp  41882  iccpartiltu  41887  iccpartigtl  41888  iccpartleu  41893  iccpartgel  41894  iccpartrn  41895  iccpartiun  41899  icceuelpart  41901  iccpartnel  41903  fargshiftf  41905  fargshiftf1  41906  pfxccatin12lem2  41953  pfxccat3  41955  fmtnoinf  41977  odz2prm2pw  42004  lighneallem4  42056  lighneal  42057  evensumeven  42145  even3prm2  42157  gbowgt5  42179  nnsum4primeseven  42217  nnsum4primesevenALTV  42218  bgoldbnnsum3prm  42221  bgoldbtbndlem2  42223  bgoldbtbndlem4  42225  bgoldbtbnd  42226  elsprel  42254  prsprel  42266  sprsymrelfo  42276  clcllaw  42356  nrhmzr  42402  rnghmmul  42429  rngccatidALTV  42518  ringccatidALTV  42581  nzerooringczr  42601  scmsuppss  42682  gsumlsscl  42693  ply1mulgsumlem2  42704  lincvalsc0  42739  linc0scn0  42741  lincdifsn  42742  linc1  42743  lincellss  42744  lincsum  42747  lincscm  42748  lincsumcl  42749  lcoss  42754  lincext3  42774  lindslinindimp2lem4  42779  lindslinindsimp2lem5  42780  lindslinindsimp2  42781  lindsrng01  42786  snlindsntor  42789  lincresunit3lem2  42798  lincresunit3  42799  islindeps2  42801  blengt1fldiv2p1  42916
  Copyright terms: Public domain W3C validator