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

Theorem expcom 414
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 413 . 2 (𝜑 → (𝜓𝜒))
32com12 32 1 (𝜓 → (𝜑𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396
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 208  df-an 397
This theorem is referenced by:  ancoms  459  pm3.21  472  sylan  580  animpimp2impd  840  4casesdan  1033  dedlema  1037  dedlemb  1038  sbiedvw  2095  cbval2vOLD  2356  cbval2OLD  2427  mo4  2646  2moswapv  2710  2moswap  2725  2mos  2730  2eu2  2734  pm2.61ne  3102  nelelne  3117  r19.21be  3210  cbvraldva2  3457  cbvrexdva2OLD  3459  rspcebdv  3616  2reu2  3881  minel  4413  uneqdifeq  4436  raltpd  4710  ssunsn2  4754  opthprneg  4789  ssuni  4854  uniss2  4864  elpwuni  5019  disjord  5046  elssabg  5231  elpw2g  5239  axprlem3  5317  axprlem4  5318  axprlem5  5319  oteqex  5382  otsndisj  5401  otiunsndisj  5402  epelg  5460  epelgOLD  5461  wereu  5545  relop  5715  riinint  5833  sotri3  5984  unixpid  6129  reuop  6138  ordtr2  6229  ordsssuc2  6273  iotan0  6339  funopg  6383  fun  6534  tz6.12c  6689  fvmptnf  6783  fvn0ssdmfun  6835  eldmrexrnb  6851  fmptco  6884  fnressn  6913  fressnfv  6915  fprb  6949  fvtp2g  6954  fvtp3g  6955  fconst2g  6958  fntpb  6964  f1dom3el3dif  7018  isores3  7077  isoselem  7083  oprabv  7203  eloprabga  7250  sorpsscmpl  7449  difex2  7470  ordpwsuc  7518  ordsucun  7528  limuni3  7555  ordom  7577  fo1stres  7706  poxp  7813  soxp  7814  suppimacnv  7832  frnsuppeq  7833  funsssuppss  7847  brtpos2  7889  wfrlem12  7957  onnseq  7972  smores  7980  smofvon2  7984  tfrlem1  8003  oacl  8151  omcl  8152  oecl  8153  oawordri  8166  oalimcl  8176  oaass  8177  oarec  8178  omwordri  8188  omeulem1  8198  omeulem2  8199  oeordi  8203  oeworde  8209  oeoelem  8214  nnacl  8227  nnmcl  8228  nnecl  8229  nnacom  8233  nnaass  8238  nnmsucr  8241  nnmordi  8247  omabs  8264  iiner  8359  elpmg  8412  pmss12g  8423  mapfvd  8433  f1domg  8518  ssdomg  8544  domtriord  8652  php  8690  php3  8692  1sdom  8710  fisseneq  8718  isinf  8720  ssnnfi  8726  dif1en  8740  findcard3  8750  frfi  8752  unfi  8774  difinf  8777  fnfi  8785  iunfi  8801  fsuppunfi  8842  fsuppres  8847  frnfsuppbi  8851  elfi2  8867  marypha1lem  8886  marypha1  8887  oiexg  8988  wemapso2  9006  harword  9018  brwdom  9020  unxpwdom  9042  en3lplem1  9064  inf3lemd  9079  inf3lem5  9084  cantnfval2  9121  cantnfle  9123  cantnflt  9124  cnfcom  9152  tcmin  9172  r1sdom  9192  rankxplim3  9299  cardidm  9377  cardmin2  9416  infxpenlem  9428  fseqenlem1  9439  numacn  9464  alephordi  9489  iscard3  9508  alephinit  9510  carduniima  9511  iunfictbso  9529  dfac5  9543  dfac12lem3  9560  pwsdompw  9615  pwdjudom  9627  cflim2  9674  cfslb2n  9679  cofsmo  9680  cfsmolem  9681  cfcoflem  9683  alephsing  9687  infpssALT  9724  fin23lem34  9757  isf32lem2  9765  isf32lem10  9773  isf32lem12  9775  isfin1-2  9796  hsmexlem4  9840  axcc2lem  9847  domtriomlem  9853  axdc2lem  9859  axdc3lem2  9862  axdc3lem4  9864  axdc4lem  9866  axcclem  9868  ac6num  9890  ac6s  9895  zorn2lem7  9913  ttukeylem5  9924  imadomg  9945  iundom2g  9951  ondomon  9974  ficard  9976  konigthlem  9979  alephreg  9993  pwcfsdom  9994  cfpwsdom  9995  axregndlem1  10013  axregnd  10015  pwfseqlem3  10071  pwxpndom2  10076  pwxpndom  10077  pwdjundom  10078  inawinalem  10100  gchina  10110  wuncval2  10158  tsk0  10174  tskxpss  10183  inatsk  10189  tskuni  10194  gruina  10229  grothac  10241  addclpi  10303  addnidpi  10312  nqereu  10340  mulcanenq  10371  genpnnp  10416  nqpr  10425  prlem934  10444  reclem2pr  10459  suplem1pr  10463  supsrlem  10522  axpre-sup  10580  1re  10630  dedekindle  10793  00id  10804  receu  11274  sup3  11587  infrelb  11615  peano5nni  11630  nnaddcl  11649  zrevaddcl  12016  nzadd  12019  zdiv  12041  nneo  12055  zeo2  12058  nn0indd  12068  fzind  12069  fnn0ind  12070  uzwo  12300  lbzbi  12325  nn01to3  12330  qrevaddcl  12360  irradd  12362  irrmul  12363  ltsubrp  12415  ltaddrp  12416  xnn0xaddcl  12618  xnn0xadd0  12630  icoshft  12849  fzen  12914  elfzm11  12968  uzsplit  12969  elfzoext  13084  elfzom1elp1fzo  13094  injresinjlem  13147  injresinj  13148  modifeq2int  13291  modsumfzodifsn  13302  om2uzlti  13308  ssnn0fi  13343  fsuppmapnn0fiub0  13351  mptnn0fsuppr  13357  seqcaopr3  13395  seqf1olem2a  13398  seqf1o  13401  ser1const  13416  expadd  13461  expmul  13464  leexp1a  13529  faccl  13633  facdiv  13637  faclbnd  13640  faclbnd4lem4  13646  hasheqf1oi  13702  hashgadd  13728  hashinfxadd  13736  hashunx  13737  hashunsng  13743  elprchashprn2  13747  hashss  13760  hash1snb  13770  hashmap  13786  hashf1lem2  13804  hashf1  13805  seqcoll  13812  hashle2pr  13825  hashdmpropge2  13831  hashge3el3dif  13834  hash1to3  13839  fundmge2nop0  13840  fi1uzind  13845  brfi1indALT  13848  sswrd  13859  swrdnd2  14007  swrdnnn0nd  14008  swrdnd0  14009  swrdwrdsymb  14014  pfxnd0  14040  swrdswrdlem  14056  swrdswrd  14057  wrd2ind  14075  swrdccatin1  14077  swrdccatin2  14081  pfxccatin12lem2  14083  pfxccat3  14086  repsdf2  14130  repswswrd  14136  cshw0  14146  cshwcl  14150  cshwlen  14151  cshf1  14162  swrdco  14189  relexpsucnnl  14381  rtrclreclem3  14409  rtrclreclem4  14410  relexpindlem  14412  rtrclind  14414  shftlem  14417  caubnd  14708  reusq0  14812  rlimcld2  14925  o1dif  14976  climub  15008  climserle  15009  iseraltlem2  15029  sumss  15071  fsumzcl2  15085  fsummsnunz  15099  fsumsplitsnun  15100  fsum2d  15116  modfsummods  15138  fsumabs  15146  fsumrlim  15156  fsumo1  15157  fsumiun  15166  climcndslem1  15194  climcndslem2  15195  cvgrat  15229  clim2prod  15234  prodfn0  15240  prodfrec  15241  ntrivcvg  15243  prodmo  15280  fprodss  15292  fprodabs  15318  fprodn0  15323  fprod2d  15325  fprodefsum  15438  ruclem8  15580  ruclem9  15581  dvdsmod0  15603  dvds2ln  15632  dvdsaddre2b  15647  dvdslelem  15649  dvdsdivcl  15656  alzdvds  15660  mod2eq1n2dvds  15686  oddnn02np1  15687  nn0o1gt2  15722  nno  15723  sumeven  15728  sumodd  15729  pwp1fsum  15732  ndvdsadd  15751  bitsinv1  15781  sadcadd  15797  sadadd2  15799  saddisjlem  15803  smuval2  15821  smupvallem  15822  smu01lem  15824  smupval  15827  smueqlem  15829  smumullem  15831  gcddiv  15889  gcdmultipleOLD  15890  rplpwr  15897  nn0seqcvgd  15904  seq1st  15905  alginv  15909  algcvga  15913  algfx  15914  absprodnn  15952  isprm2  16016  isprm3  16017  prmind2  16019  maxprmfct  16043  prmdvdsexp  16049  pcmpt  16218  prmreclem4  16245  vdwmc2  16305  vdwlem10  16316  ramub2  16340  ramcl  16355  prmgaplem5  16381  prmgaplem8  16384  cshwshashlem1  16419  cshwshashlem3  16421  setsn0fun  16510  imasleval  16804  divsfval  16810  mreexexlem4d  16908  isssc  17080  initoeu1  17261  termoeu1  17268  istos  17635  mgmcl  17845  sgrpidmnd  17906  frmdgsum  18017  dfgrp3lem  18137  mhmmulg  18208  resghm2b  18316  gsumwrev  18434  elsymgbas  18440  symgextf1  18480  gsmsymgreqlem2  18490  gsmsymgreq  18491  odlem1  18594  odcl2  18623  gexlem1  18635  efgi2  18782  efginvrel2  18784  efgsrel  18791  cyggexb  18950  gsummulglem  18992  gsumzunsnd  19007  gsum2dlem2  19022  telgsums  19044  dmdprd  19051  dprdw  19063  ablfac1eulem  19125  srgpcomp  19213  lmodfopnelem1  19601  rmodislmodlem  19632  mplcoe1  20176  mplcoe3  20177  mplcoe5  20179  cply1mul  20392  coe1fzgsumdlem  20399  gsummoncoe1  20402  pf1ind  20448  evl1gsumdlem  20449  cnfldmulg  20507  cnfldexp  20508  obslbs  20804  mat1dimcrng  21016  ma1repveval  21110  mulmarep1gsum2  21113  gsummatr01lem3  21196  cramerlem3  21228  decpmatmulsumfsupp  21311  mp2pm2mplem4  21347  pm2mpmhmlem1  21356  fvmptnn04if  21387  cayhamlem1  21404  fctop  21542  mretopd  21630  restopnb  21713  restdis  21716  tgcnp  21791  cncls2  21811  cncls  21812  cnntr  21813  cnsscnp  21817  cmpsub  21938  2ndcsep  21997  1stcelcls  21999  lfinpfin  22062  locfincmp  22064  comppfsc  22070  txcn  22164  txlm  22186  xkohaus  22191  qtopres  22236  haushmphlem  22325  cmphmph  22326  connhmph  22327  reghmph  22331  nrmhmph  22332  ptcmpfi  22351  reghaus  22363  fbssfi  22375  fbun  22378  fbfinnfr  22379  isfildlem  22395  fgcl  22416  cfinfil  22431  supfil  22433  ufinffr  22467  fin1aufil  22470  cnpflf  22539  alexsubALTlem3  22587  alexsubALT  22589  cnextfvval  22603  cnextcn  22605  tmdgsum  22633  tgphaus  22654  tgpt1  22655  mettri  22891  blssexps  22965  blssex  22966  mopni3  23033  metss  23047  psmetutop  23106  dscmet  23111  tngngp3  23194  rectbntr0  23369  metnrmlem1a  23395  fsumcn  23407  lmmbr  23790  caubl  23840  caublcls  23841  bcthlem5  23860  bcth3  23863  ovolunlem1a  24026  ovoliunnul  24037  finiunmbl  24074  voliunlem1  24080  volsuplem  24085  volsup  24086  dyadmax  24128  itgfsum  24356  dvnadd  24455  cpnord  24461  dvnfre  24478  dvmptfsum  24501  dvlip  24519  fta1g  24690  plyco  24760  dgrcolem1  24792  dgrco  24794  dvnply2  24805  plydivex  24815  plyexmo  24831  aannenlem1  24846  aaliou3lem2  24861  dvntaylp  24888  taylthlem1  24890  ulmval  24897  cxpmul2  25199  cxpsqrtth  25239  scvxcvx  25491  jensenlem2  25493  jensen  25494  ppiub  25708  bcmono  25781  bpos1lem  25786  bposlem5  25792  gausslemma2dlem6  25876  lgsquad2lem2  25889  2lgslem3  25908  2lgs  25911  2sqnn  25943  addsqnreup  25947  2sqreultblem  25952  2sqreunnltblem  25955  dchrisumlem1  25993  dchrisum0flb  26014  pntpbnd1  26090  pntlemf  26109  qabvle  26129  qabvexp  26130  ostthlem2  26132  ostth2lem2  26138  axeuclidlem  26676  axcontlem12  26689  umgrnloopv  26819  uhgredgrnv  26843  edglnl  26856  numedglnl  26857  usgruspgrb  26894  usgrnloopvALT  26911  usgredg2vlem2  26936  subupgr  26997  nbumgr  27057  uhgrnbgr0nb  27064  nbgr0vtxlem  27065  edgusgrnbfin  27083  nb3grprlem2  27091  uvtxnbgrvtx  27103  cplgrop  27147  cusgrfi  27168  fusgrmaxsize  27174  fusgrn0degnn0  27209  ewlkprop  27313  uspgr2wlkeq  27355  g0wlk0  27361  wlkreslem  27379  lfgriswlk  27398  upgrwlkdvde  27446  spthonepeq  27461  uhgrwkspth  27464  usgr2trlncl  27469  usgr2trlspth  27470  cyclnspth  27509  crctcshwlkn0lem3  27518  wwlksn  27543  wspthneq1eq2  27566  wwlksm1edg  27587  wwlksnred  27598  wwlksnextfun  27604  wwlksnextinj  27605  wwlksnextproplem3  27618  wspthsnonn0vne  27624  wspn0  27631  rusgrnumwwlk  27682  clwwlkccatlem  27695  umgrclwwlkge2  27697  clwlkclwwlklem2  27706  clwlkclwwlklem3  27707  clwwisshclwws  27721  clwwisshclwwsn  27722  clwwlkn1loopb  27749  clwwlknfiOLD  27752  wwlksext2clwwlk  27764  wwlksubclwwlk  27765  clwwlknonex2lem2  27815  upgr3v3e3cycl  27887  uhgr3cyclex  27889  upgr4cycl4dv4e  27892  eupth2lem3lem4  27938  eupth2lem3lem7  27941  eupth2  27946  eulerpath  27948  nfrgr2v  27979  frgr3vlem1  27980  3vfriswmgr  27985  1to2vfriswmgr  27986  1to3vfriswmgr  27987  3cyclfrgrrn1  27992  3cyclfrgrrn  27993  3cyclfrgrrn2  27994  4cycl2vnunb  27997  frgrncvvdeqlem2  28007  frgrncvvdeqlem8  28013  frgrncvvdeqlem9  28014  frgrwopreglem4a  28017  frgrwopreglem5lem  28027  frgrwopreglem5ALT  28029  frgrregorufr0  28031  frgr2wwlk1  28036  frgr2wwlkeqm  28038  fusgr2wsp2nb  28041  2wspmdisj  28044  frrusgrord  28048  numclwwlk1lem2f1  28064  numclwlk1  28078  frgrreggt1  28100  friendshipgt3  28105  hlim2  28897  elnlfn  29633  stle0i  29944  hstrbi  29971  spansncv2  29998  h1da  30054  fmptcof2  30331  nnindd  30463  xreceu  30526  tpr2rico  31055  hasheuni  31244  ismeas  31358  sseqp1  31553  rrvsum  31612  dstfrvunirn  31632  sgn3da  31699  signstfvc  31744  bnj607  32088  bnj1145  32163  bnj1204  32182  fisshasheq  32250  subgrwlk  32277  subfacp1lem6  32330  cvmlift2lem12  32459  cvmlift3lem4  32467  satfrnmapom  32515  sat1el2xp  32524  satffunlem2  32553  satffun  32554  mrsubvrs  32667  climuzcnv  32812  iprodefisumlem  32870  dfon2lem9  32934  trpredtr  32967  trpredmintr  32968  dftrpred3g  32970  trpredrec  32975  soseq  32994  frrlem8  33028  fpr2  33038  frr2  33043  sltval2  33061  sltsolem1  33078  linethru  33512  elhf2  33534  finminlem  33564  fnessref  33603  neibastop2lem  33606  fnemeet2  33613  nndivsub  33703  bj-xpnzex  34169  bj-elpwg  34240  bj-epelg  34255  bj-intss  34286  mptsnunlem  34502  dissneqlem  34504  topdifinffinlem  34511  iooelexlt  34526  domalom  34568  fvineqsneq  34576  wl-exeq  34656  wl-ax11-lem3  34701  matunitlindflem1  34770  poimirlem22  34796  poimirlem26  34800  poimirlem28  34802  poimirlem29  34803  poimirlem32  34806  heicant  34809  ovoliunnfl  34816  voliunnfl  34818  volsupnfl  34819  cover2  34872  upixp  34887  sdclem2  34900  fdc  34903  seqpo  34905  metf1o  34913  mettrifi  34915  sstotbnd3  34937  heibor1lem  34970  heiborlem5  34976  heibor  34982  bfplem1  34983  elghomlem2OLD  35047  grpokerinj  35054  isrngo  35058  rngodm1dm2  35093  ispridl2  35199  exlimddvf  35282  lssatle  36033  4atexlemex4  37091  sn-axprlem3  38989  mzpsubst  39225  jm2.18  39465  wepwsolem  39522  iunrelexp0  39927  relexpmulg  39935  cnvtrclfv  39949  clsk1indlem3  40273  grucollcld  40476  inaex  40513  dvgrat  40524  radcnvrat  40526  csbxpgVD  41108  sineq0ALT  41151  islptre  41780  iblspltprt  42138  stoweidlem2  42168  stoweidlem17  42183  stoweidlem21  42187  2reuimp0  43194  2reuimp  43195  afveu  43233  funbrafv  43238  ndmaovass  43286  afv2eu  43318  tz6.12c-afv2  43322  funop1  43363  f1oresf1o2  43371  fvmptrabdm  43373  nltle2tri  43394  2elfz2melfz  43399  fzoopth  43408  fsummsndifre  43413  fsumsplitsndif  43414  fsummmodsndifre  43415  fsummmodsnunz  43416  iccpartiltu  43429  iccpartigtl  43430  iccpartleu  43435  iccpartgel  43436  iccpartrn  43437  iccpartiun  43441  icceuelpart  43443  iccpartnel  43445  fargshiftf  43447  fargshiftf1  43448  ichnfb  43472  elsprel  43484  prsprel  43496  sprsymrelfo  43506  paireqne  43520  sbcpr  43530  reupr  43531  fmtnoinf  43545  odz2prm2pw  43572  lighneallem4  43622  lighneal  43623  requad1  43634  requad2  43635  evensumeven  43719  even3prm2  43731  gbowgt5  43774  nnsum4primeseven  43812  nnsum4primesevenALTV  43813  bgoldbnnsum3prm  43816  bgoldbtbndlem2  43818  bgoldbtbndlem4  43820  bgoldbtbnd  43821  isomuspgrlem1  43839  smndex1mgm  43977  clcllaw  43996  nrhmzr  44042  rnghmmul  44069  rngccatidALTV  44158  ringccatidALTV  44221  nzerooringczr  44241  scmsuppss  44318  gsumlsscl  44329  ply1mulgsumlem2  44339  lincvalsc0  44374  linc0scn0  44376  lincdifsn  44377  linc1  44378  lincellss  44379  lincsum  44382  lincscm  44383  lincsumcl  44384  lcoss  44389  lincext3  44409  lindslinindimp2lem4  44414  lindslinindsimp2lem5  44415  lindslinindsimp2  44416  lindsrng01  44421  snlindsntor  44424  lincresunit3lem2  44433  lincresunit3  44434  islindeps2  44436  blengt1fldiv2p1  44551  resum2sqorgt0  44594  reorelicc  44595  rrx2plordisom  44608  rrx2linest  44627  rrxsphere  44633  line2ylem  44636  itsclc0xyqsol  44653  itscnhlinecirc02p  44670
  Copyright terms: Public domain W3C validator