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

Theorem expcom 451
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 450 . 2 (𝜑 → (𝜓𝜒))
32com12 32 1 (𝜓 → (𝜑𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384
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 386
This theorem is referenced by:  ancoms  469  syldan  487  sylan  488  4casesdan  990  dedlema  1001  dedlemb  1002  cbval2  2278  cbvaldva  2280  2moswap  2546  2eu2  2553  pm2.61ne  2875  nelelne  2888  r19.21be  2929  minel  4011  uneqdifeq  4035  uneqdifeqOLD  4036  raltpd  4292  ssunsn2  4334  ssuni  4432  ssuniOLD  4433  uniss2  4443  elpwuni  4589  elssabg  4789  elpw2g  4797  oteqex  4934  otsndisj  4949  otiunsndisj  4950  epelg  4996  wereu  5080  relop  5242  riinint  5352  sotri3  5495  unixpid  5639  ordtr2  5737  ordsssuc2  5783  funopg  5890  fun  6033  tz6.12c  6180  fvmptnf  6268  fvn0ssdmfun  6316  eldmrexrnb  6332  fmptco  6362  funopsn  6378  fnressn  6390  fressnfv  6392  fvtp2g  6429  fvtp3g  6430  fconst2g  6433  fntpb  6438  f1dom3el3dif  6491  isores3  6550  isoselem  6556  oprabv  6668  eloprabga  6712  sorpsscmpl  6913  difex2  6933  ordpwsuc  6977  ordsucun  6987  limuni3  7014  ordom  7036  fo1stres  7152  poxp  7249  soxp  7250  suppimacnv  7266  frnsuppeq  7267  funsssuppss  7281  brtpos2  7318  wfrlem12  7386  onnseq  7401  smores  7409  smofvon2  7413  tfrlem1  7432  oacl  7575  omcl  7576  oecl  7577  oawordri  7590  oalimcl  7600  oaass  7601  oarec  7602  omwordri  7612  omeulem1  7622  omeulem2  7623  oeordi  7627  oeworde  7633  oeoelem  7638  nnacl  7651  nnmcl  7652  nnecl  7653  nnacom  7657  nnaass  7662  nnmsucr  7665  nnmordi  7671  omabs  7687  iiner  7779  elpmg  7833  pmss12g  7844  mapsn  7859  f1domg  7935  ssdomg  7961  domtriord  8066  php  8104  php3  8106  1sdom  8123  fisseneq  8131  isinf  8133  ssnnfi  8139  dif1en  8153  findcard3  8163  frfi  8165  unfi  8187  difinf  8190  fnfi  8198  iunfi  8214  fsuppunfi  8255  fsuppres  8260  frnfsuppbi  8264  elfi2  8280  marypha1lem  8299  marypha1  8300  oiexg  8400  wemapso2  8418  harword  8430  brwdom  8432  unxpwdom  8454  en3lplem1  8471  inf3lemd  8484  inf3lem5  8489  cantnfval2  8526  cantnfle  8528  cantnflt  8529  cnfcom  8557  tcmin  8577  r1sdom  8597  rankxplim3  8704  cardidm  8745  cardmin2  8784  infxpenlem  8796  fseqenlem1  8807  numacn  8832  alephordi  8857  iscard3  8876  alephinit  8878  carduniima  8879  iunfictbso  8897  dfac5  8911  dfac12lem3  8927  pwsdompw  8986  pwcdadom  8998  cflim2  9045  cfslb2n  9050  cofsmo  9051  cfsmolem  9052  cfcoflem  9054  alephsing  9058  infpssALT  9095  fin23lem34  9128  isf32lem2  9136  isf32lem10  9144  isf32lem12  9146  isfin1-2  9167  hsmexlem4  9211  axcc2lem  9218  domtriomlem  9224  axdc2lem  9230  axdc3lem2  9233  axdc3lem4  9235  axdc4lem  9237  axcclem  9239  ac6num  9261  ac6s  9266  zorn2lem7  9284  ttukeylem5  9295  imadomg  9316  iundom2g  9322  ondomon  9345  ficard  9347  konigthlem  9350  alephreg  9364  pwcfsdom  9365  cfpwsdom  9366  axregndlem1  9384  axregnd  9386  pwfseqlem3  9442  pwxpndom2  9447  pwxpndom  9448  pwcdandom  9449  inawinalem  9471  gchina  9481  wuncval2  9529  tsk0  9545  tskxpss  9554  inatsk  9560  tskuni  9565  gruina  9600  grothac  9612  addclpi  9674  addnidpi  9683  nqereu  9711  mulcanenq  9742  genpnnp  9787  nqpr  9796  prlem934  9815  reclem2pr  9830  suplem1pr  9834  supsrlem  9892  axpre-sup  9950  1re  9999  dedekindle  10161  00id  10171  receu  10632  sup3  10940  infrelb  10968  peano5nni  10983  nnaddcl  11002  zrevaddcl  11382  nzadd  11385  zdiv  11407  nneo  11421  zeo2  11424  nn0indd  11434  fzind  11435  fnn0ind  11436  uzwo  11711  lbzbi  11736  nn01to3  11741  qrevaddcl  11770  irradd  11772  irrmul  11773  ltsubrp  11826  ltaddrp  11827  xnn0xaddcl  12025  xnn0xadd0  12036  icoshft  12252  fzen  12316  elfzm11  12368  uzsplit  12369  elfzoext  12481  elfzom1elp1fzo  12491  injresinjlem  12544  injresinj  12545  modifeq2int  12688  modsumfzodifsn  12699  om2uzlti  12705  ssnn0fi  12740  fsuppmapnn0fiub0  12749  mptnn0fsuppr  12755  seqcl2  12775  seqfveq2  12779  seqshft2  12783  monoord  12787  seqsplit  12790  seqcaopr3  12792  seqf1olem2a  12795  seqf1o  12798  seqid2  12803  seqhomo  12804  ser1const  12813  expadd  12858  expmul  12861  leexp1a  12875  faccl  13026  facdiv  13030  faclbnd  13033  faclbnd4lem4  13039  faclbnd6  13042  hasheqf1oi  13096  hasheqf1oiOLD  13097  hashf1rnOLD  13099  hashgadd  13122  hashinfxadd  13130  hashunx  13131  hashunsng  13137  elprchashprn2  13140  hashss  13153  hash1snb  13163  hashmap  13178  hashf1lem2  13194  hashf1  13195  seqcoll  13202  hashle2pr  13213  hashdmpropge2  13219  hashge3el3dif  13222  hash1to3  13228  fundmge2nop0  13229  fi1uzind  13234  brfi1indALT  13237  fi1uzindOLD  13240  brfi1indALTOLD  13243  sswrd  13268  swrdnd2  13387  swrdswrdlem  13413  swrdswrd  13414  wrd2ind  13431  swrdccatin1  13436  swrdccatin2  13440  swrdccatin12lem2  13442  swrdccat3  13445  repsdf2  13478  repswswrd  13484  cshw0  13493  cshwcl  13497  cshwlen  13498  cshf1  13509  swrdco  13536  relexpsucnnl  13722  rtrclreclem3  13750  rtrclreclem4  13751  relexpindlem  13753  rtrclind  13755  shftlem  13758  caubnd  14048  rlimcld2  14259  o1dif  14310  climub  14342  climserle  14343  iseraltlem2  14363  sumss  14404  fsumzcl2  14418  fsummsnunz  14432  fsumsplitsnun  14433  fsum2d  14449  modfsummods  14471  fsumabs  14479  fsumrlim  14489  fsumo1  14490  fsumiun  14499  bcxmas  14511  climcndslem1  14525  climcndslem2  14526  cvgrat  14559  clim2prod  14564  prodfn0  14570  prodfrec  14571  ntrivcvg  14573  prodmo  14610  fprodss  14622  fprodabs  14648  fprodn0  14653  fprod2d  14655  fprodefsum  14769  ruclem8  14910  ruclem9  14911  dvds2ln  14957  dvdsaddre2b  14972  dvdslelem  14974  dvdsdivcl  14981  alzdvds  14985  mod2eq1n2dvds  15014  oddnn02np1  15015  nn0o1gt2  15040  nno  15041  sumeven  15053  sumodd  15054  pwp1fsum  15057  ndvdsadd  15077  bitsinv1  15107  sadcadd  15123  sadadd2  15125  saddisjlem  15129  smuval2  15147  smupvallem  15148  smu01lem  15150  smupval  15153  smueqlem  15155  smumullem  15157  gcddiv  15211  gcdmultiple  15212  rplpwr  15219  nn0seqcvgd  15226  seq1st  15227  alginv  15231  algcvga  15235  algfx  15236  absprodnn  15274  isprm2  15338  isprm3  15339  prmind2  15341  maxprmfct  15364  prmdvdsexp  15370  pcmpt  15539  prmreclem4  15566  vdwmc2  15626  vdwlem10  15637  ramub2  15661  ramcl  15676  prmgaplem5  15702  prmgaplem8  15705  cshwshashlem1  15745  cshwshashlem3  15747  setsn0fun  15835  imasleval  16141  divsfval  16147  mreexexlem4d  16247  isssc  16420  initoeu1  16601  termoeu1  16608  istos  16975  mgmcl  17185  frmdgsum  17339  dfgrp3lem  17453  mhmmulg  17523  resghm2b  17618  gsumwrev  17736  elsymgbas  17742  symgextf1  17781  gsmsymgreqlem2  17791  gsmsymgreq  17792  odlem1  17894  odcl2  17922  gexlem1  17934  sylow1lem1  17953  efgi2  18078  efginvrel2  18080  efgsrel  18087  cyggexb  18240  gsummulglem  18281  gsumzunsnd  18295  gsum2dlem2  18310  telgsums  18330  dmdprd  18337  dprdw  18349  ablfac1eulem  18411  srgpcomp  18472  lmodfopnelem1  18839  rmodislmodlem  18870  mplcoe1  19405  mplcoe3  19406  mplcoe5  19408  cply1mul  19604  coe1fzgsumdlem  19611  gsummoncoe1  19614  pf1ind  19659  evl1gsumdlem  19660  cnfldmulg  19718  cnfldexp  19719  obslbs  20014  mat1dimcrng  20223  ma1repveval  20317  mulmarep1gsum2  20320  gsummatr01lem3  20403  cramerlem3  20435  decpmatmulsumfsupp  20518  mp2pm2mplem4  20554  pm2mpmhmlem1  20563  fvmptnn04if  20594  cayhamlem1  20611  fctop  20748  mretopd  20836  restopnb  20919  restdis  20922  tgcnp  20997  cncls2  21017  cncls  21018  cnntr  21019  cnsscnp  21023  cmpsub  21143  2ndcsep  21202  1stcelcls  21204  lfinpfin  21267  locfincmp  21269  comppfsc  21275  txcn  21369  txlm  21391  xkohaus  21396  qtopres  21441  haushmphlem  21530  cmphmph  21531  connhmph  21532  reghmph  21536  nrmhmph  21537  ptcmpfi  21556  reghaus  21568  fbssfi  21581  fbun  21584  fbfinnfr  21585  isfildlem  21601  fgcl  21622  cfinfil  21637  supfil  21639  ufinffr  21673  fin1aufil  21676  cnpflf  21745  alexsubALTlem3  21793  alexsubALT  21795  cnextfvval  21809  cnextcn  21811  tmdmulg  21836  tmdgsum  21839  tgphaus  21860  tgpt1  21861  mettri  22097  imasdsf1olem  22118  blssexps  22171  blssex  22172  mopni3  22239  metss  22253  psmetutop  22312  dscmet  22317  tngngp3  22400  rectbntr0  22575  metnrmlem1a  22601  fsumcn  22613  lmmbr  22996  caubl  23046  caublcls  23047  bcthlem5  23065  bcth3  23068  ovolunlem1a  23204  ovoliunnul  23215  ovolicc2lem3  23227  finiunmbl  23252  voliunlem1  23258  volsuplem  23263  volsup  23264  dyadmax  23306  itgfsum  23533  dvnadd  23632  dvnres  23634  cpnord  23638  dvnfre  23655  dvmptfsum  23676  dvlip  23694  fta1g  23865  plyco  23935  dgrcolem1  23967  dgrco  23969  dvnply2  23980  plydivex  23990  plyexmo  24006  aannenlem1  24021  aaliou3lem2  24036  dvntaylp  24063  taylthlem1  24065  ulmval  24072  cxpmul2  24369  scvxcvx  24646  jensenlem2  24648  jensen  24649  ppiub  24863  bcmono  24936  bpos1lem  24941  bposlem5  24947  gausslemma2dlem6  25031  lgsquad2lem2  25044  2lgslem3  25063  2lgs  25066  dchrisumlem1  25112  dchrisum0flb  25133  pntpbnd1  25209  pntlemf  25228  qabvle  25248  qabvexp  25249  ostthlem2  25251  ostth2lem2  25257  axeuclidlem  25776  axcontlem12  25789  umgrnloopv  25930  uhgredgrnv  25954  usgruspgrb  26003  usgrnloopvALT  26020  usgredg2vlem2  26045  subupgr  26106  nbumgr  26164  uhgrnbgr0nb  26171  nbgr0vtxlem  26172  edgusgrnbfin  26196  nb3grprlem2  26204  uvtxanbgrvtx  26214  cplgrop  26254  cusgrfi  26275  fusgrmaxsize  26281  fusgrn0degnn0  26315  ewlkprop  26403  uspgr2wlkeq  26445  g0wlk0  26451  wlkreslem  26469  wlkres  26470  lfgriswlk  26488  upgrwlkdvde  26536  spthonepeq  26551  uhgrwkspth  26554  usgr2trlncl  26559  usgr2trlspth  26560  cyclnspth  26598  crctcshwlkn0lem3  26607  wwlksn  26632  wspthneq1eq2  26648  wwlksm1edg  26670  wwlksnred  26690  wwlksnextfun  26696  wwlksnextinj  26697  wwlksnextproplem3  26709  wspthsnonn0vne  26716  rusgrnumwwlk  26771  clwwlksn  26782  clwlkclwwlklem2  26802  clwlkclwwlklem3  26803  umgrclwwlksge2  26812  wwlksubclwwlks  26825  clwwisshclwws  26828  clwwisshclwwsn  26829  clwlksfclwwlk  26862  upgr3v3e3cycl  26940  uhgr3cyclex  26942  upgr4cycl4dv4e  26945  eupthseg  26966  upgreupthseg  26969  eupth2lem3lem4  26991  eupth2lem3lem7  26994  eupth2  26999  eulerpath  27001  nfrgr2v  27034  frgr3vlem1  27035  3vfriswmgr  27040  1to2vfriswmgr  27041  1to3vfriswmgr  27042  3cyclfrgrrn1  27047  3cyclfrgrrn  27048  3cyclfrgrrn2  27049  4cycl2vnunb  27052  frgrncvvdeqlem4  27064  frgrncvvdeqlemB  27069  frgrncvvdeqlemC  27070  frgrwopreglem4  27076  frgrwopreg  27078  frgrregorufr0  27081  frgreu  27083  frgr2wwlk1  27086  fusgr2wsp2nb  27090  2wspmdisj  27093  fusgreghash2wsp  27094  numclwwlkovf2ex  27109  numclwlk1lem2foa  27113  numclwlk1lem2f1  27116  frgrreggt1  27139  friendshipgt3  27144  hlim2  27937  elnlfn  28675  stle0i  28986  hstrbi  29013  spansncv2  29040  h1da  29096  fmptcof2  29340  nnindd  29449  xreceu  29457  tpr2rico  29782  hasheuni  29970  ismeas  30085  sseqp1  30280  rrvsum  30339  dstfrvunirn  30359  sgn3da  30426  bnj607  30747  bnj1145  30822  bnj1204  30841  subfacp1lem6  30928  cvmliftlem7  31034  cvmliftlem10  31037  cvmlift2lem12  31057  cvmlift3lem4  31065  mrsubvrs  31180  climuzcnv  31326  iprodefisumlem  31387  fprb  31426  dfon2lem9  31450  trpredtr  31484  trpredmintr  31485  dftrpred3g  31487  trpredrec  31492  soseq  31505  frrlem11  31546  sltval2  31563  sltsolem1  31581  linethru  31955  elhf2  31977  finminlem  32007  fnessref  32047  neibastop2lem  32050  fnemeet2  32057  nndivsub  32151  bj-cbval2v  32432  bj-xpnzex  32646  mptsnunlem  32856  dissneqlem  32858  topdifinffinlem  32866  iooelexlt  32881  wl-exeq  32992  wl-ax11-lem3  33035  matunitlindflem1  33076  poimirlem22  33102  poimirlem26  33106  poimirlem28  33108  poimirlem29  33109  poimirlem32  33112  heicant  33115  ovoliunnfl  33122  voliunnfl  33124  volsupnfl  33125  cover2  33179  upixp  33195  sdclem2  33209  fdc  33212  seqpo  33214  metf1o  33222  mettrifi  33224  sstotbnd3  33246  heibor1lem  33279  heiborlem5  33285  heibor  33291  bfplem1  33292  elghomlem2OLD  33356  grpokerinj  33363  isrngo  33367  rngodm1dm2  33402  ispridl2  33508  exlimddvf  33597  lssatle  33821  4atexlemex4  34878  mzpsubst  36830  jm2.18  37074  wepwsolem  37131  iunrelexp0  37514  relexpmulg  37522  cnvtrclfv  37536  clsk1indlem3  37862  dvgrat  38032  radcnvrat  38034  sbcoreleleqVD  38617  csbxpgVD  38652  sineq0ALT  38695  islptre  39287  iblspltprt  39526  stoweidlem2  39556  stoweidlem17  39571  stoweidlem21  39575  2reu2  40521  afveu  40567  funbrafv  40572  ndmaovass  40620  funop1  40629  nltle2tri  40650  2elfz2melfz  40655  fzoopth  40664  smonoord  40669  fsummsndifre  40670  fsumsplitsndif  40671  fsummmodsndifre  40672  fsummmodsnunz  40673  iccpartimp  40681  iccpartiltu  40686  iccpartigtl  40687  iccpartleu  40692  iccpartgel  40693  iccpartrn  40694  iccpartiun  40698  icceuelpart  40700  iccpartnel  40702  fargshiftf  40704  fargshiftf1  40705  pfxccatin12lem2  40753  pfxccat3  40755  fmtnoinf  40777  odz2prm2pw  40804  lighneallem4  40856  lighneal  40857  evensumeven  40945  gbogt5  40975  nnsum4primeseven  41007  nnsum4primesevenALTV  41008  bgoldbnnsum3prm  41011  bgoldbtbndlem2  41013  bgoldbtbndlem4  41015  bgoldbtbnd  41016  elsprel  41043  prsprel  41055  sprsymrelfo  41065  clcllaw  41145  nrhmzr  41191  rnghmmul  41218  rngccatidALTV  41307  ringccatidALTV  41370  nzerooringczr  41390  scmsuppss  41471  gsumlsscl  41482  ply1mulgsumlem2  41493  lincvalsc0  41528  linc0scn0  41530  lincdifsn  41531  linc1  41532  lincellss  41533  lincsum  41536  lincscm  41537  lincsumcl  41538  lcoss  41543  lincext3  41563  lindslinindimp2lem4  41568  lindslinindsimp2lem5  41569  lindslinindsimp2  41570  lindsrng01  41575  snlindsntor  41578  lincresunit3lem2  41587  lincresunit3  41588  islindeps2  41590  blengt1fldiv2p1  41709
  Copyright terms: Public domain W3C validator