Theorem expcom 400

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

Step	Hyp	Ref	Expression
1		ex.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
2	1	ex 399	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3	2	com12 32	1 ⊢ (𝜓 → (𝜑 → 𝜒))

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 198  df-an 385

This theorem is referenced by:  ancoms  448  pm3.21  459  sylan  571  syldan  581  animpimp2impd  864  4casesdan  1055  dedlema  1059  dedlemb  1060  cbval2  2450  cbvaldva  2452  2moswap  2711  2eu2  2718  pm2.61ne  3063  nelelne  3076  r19.21be  3121  rspcebdv  3507  minel  4230  uneqdifeq  4253  raltpd  4504  ssunsn2  4548  opthprneg  4587  ssuni  4654  uniss2  4664  elpwuni  4808  disjord  4833  elssabg  5011  elpw2g  5019  oteqex  5153  otsndisj  5174  otiunsndisj  5175  epelg  5225  wereu  5307  relop  5474  riinint  5583  sotri3  5737  unixpid  5884  ordtr2  5981  ordsssuc2  6027  funopg  6135  fun  6281  tz6.12c  6433  fvmptnf  6523  fvn0ssdmfun  6572  eldmrexrnb  6588  fmptco  6619  fnressn  6649  fressnfv  6651  fvtp2g  6689  fvtp3g  6690  fconst2g  6693  fntpb  6698  f1dom3el3dif  6750  isores3  6809  isoselem  6815  oprabv  6933  eloprabga  6977  sorpsscmpl  7178  difex2  7199  ordpwsuc  7245  ordsucun  7255  limuni3  7282  ordom  7304  fo1stres  7424  poxp  7523  soxp  7524  suppimacnv  7540  frnsuppeq  7541  funsssuppss  7556  brtpos2  7593  wfrlem12  7662  onnseq  7677  smores  7685  smofvon2  7689  tfrlem1  7708  oacl  7852  omcl  7853  oecl  7854  oawordri  7867  oalimcl  7877  oaass  7878  oarec  7879  omwordri  7889  omeulem1  7899  omeulem2  7900  oeordi  7904  oeworde  7910  oeoelem  7915  nnacl  7928  nnmcl  7929  nnecl  7930  nnacom  7934  nnaass  7939  nnmsucr  7942  nnmordi  7948  omabs  7964  iiner  8054  elpmg  8108  pmss12g  8119  f1domg  8212  ssdomg  8238  domtriord  8345  php  8383  php3  8385  1sdom  8402  fisseneq  8410  isinf  8412  ssnnfi  8418  dif1en  8432  findcard3  8442  frfi  8444  unfi  8466  difinf  8469  fnfi  8477  iunfi  8493  fsuppunfi  8534  fsuppres  8539  frnfsuppbi  8543  elfi2  8559  marypha1lem  8578  marypha1  8579  oiexg  8679  wemapso2  8697  harword  8709  brwdom  8711  unxpwdom  8733  en3lplem1  8754  inf3lemd  8771  inf3lem5  8776  cantnfval2  8813  cantnfle  8815  cantnflt  8816  cnfcom  8844  tcmin  8864  r1sdom  8884  rankxplim3  8991  cardidm  9068  cardmin2  9107  infxpenlem  9119  fseqenlem1  9130  numacn  9155  alephordi  9180  iscard3  9199  alephinit  9201  carduniima  9202  iunfictbso  9220  dfac5  9234  dfac12lem3  9252  pwsdompw  9311  pwcdadom  9323  cflim2  9370  cfslb2n  9375  cofsmo  9376  cfsmolem  9377  cfcoflem  9379  alephsing  9383  infpssALT  9420  fin23lem34  9453  isf32lem2  9461  isf32lem10  9469  isf32lem12  9471  isfin1-2  9492  hsmexlem4  9536  axcc2lem  9543  domtriomlem  9549  axdc2lem  9555  axdc3lem2  9558  axdc3lem4  9560  axdc4lem  9562  axcclem  9564  ac6num  9586  ac6s  9591  zorn2lem7  9609  ttukeylem5  9620  imadomg  9641  iundom2g  9647  ondomon  9670  ficard  9672  konigthlem  9675  alephreg  9689  pwcfsdom  9690  cfpwsdom  9691  axregndlem1  9709  axregnd  9711  pwfseqlem3  9767  pwxpndom2  9772  pwxpndom  9773  pwcdandom  9774  inawinalem  9796  gchina  9806  wuncval2  9854  tsk0  9870  tskxpss  9879  inatsk  9885  tskuni  9890  gruina  9925  grothac  9937  addclpi  9999  addnidpi  10008  nqereu  10036  mulcanenq  10067  genpnnp  10112  nqpr  10121  prlem934  10140  reclem2pr  10155  suplem1pr  10159  supsrlem  10217  axpre-sup  10275  1re  10325  dedekindle  10486  00id  10496  receu  10957  sup3  11265  infrelb  11293  peano5nni  11308  nnaddcl  11327  zrevaddcl  11688  nzadd  11691  zdiv  11713  nneo  11727  zeo2  11730  nn0indd  11740  fzind  11741  fnn0ind  11742  uzwo  11970  lbzbi  11995  nn01to3  12000  qrevaddcl  12029  irradd  12031  irrmul  12032  ltsubrp  12080  ltaddrp  12081  xnn0xaddcl  12284  xnn0xadd0  12295  icoshft  12515  fzen  12581  elfzm11  12634  uzsplit  12635  elfzoext  12749  elfzom1elp1fzo  12759  injresinjlem  12812  injresinj  12813  modifeq2int  12956  modsumfzodifsn  12967  om2uzlti  12973  ssnn0fi  13008  fsuppmapnn0fiub0  13016  mptnn0fsuppr  13022  seqcaopr3  13059  seqf1olem2a  13062  seqf1o  13065  ser1const  13080  expadd  13125  expmul  13128  leexp1a  13142  faccl  13290  facdiv  13294  faclbnd  13297  faclbnd4lem4  13303  faclbnd6  13306  hasheqf1oi  13360  hashgadd  13384  hashinfxadd  13392  hashunx  13393  hashunsng  13399  elprchashprn2  13401  hashss  13414  hash1snb  13424  hashmap  13439  hashf1lem2  13457  hashf1  13458  seqcoll  13465  hashle2pr  13476  hashdmpropge2  13482  hashge3el3dif  13485  hash1to3  13490  fundmge2nop0  13491  fi1uzind  13496  brfi1indALT  13499  sswrd  13524  swrdnd2  13657  swrdswrdlem  13683  swrdswrd  13684  wrd2ind  13701  swrdccatin1  13707  swrdccatin2  13711  swrdccatin12lem2  13713  swrdccat3  13716  repsdf2  13749  repswswrd  13755  cshw0  13764  cshwcl  13768  cshwlen  13769  cshf1  13780  swrdco  13807  relexpsucnnl  13995  rtrclreclem3  14023  rtrclreclem4  14024  relexpindlem  14026  rtrclind  14028  shftlem  14031  caubnd  14321  rlimcld2  14532  o1dif  14583  climub  14615  climserle  14616  iseraltlem2  14636  sumss  14678  fsumzcl2  14692  fsummsnunz  14706  fsumsplitsnun  14707  fsummsnunzOLD  14708  fsumsplitsnunOLD  14709  fsum2d  14725  modfsummods  14747  fsumabs  14755  fsumrlim  14765  fsumo1  14766  fsumiun  14775  bcxmas  14789  climcndslem1  14803  climcndslem2  14804  cvgrat  14836  clim2prod  14841  prodfn0  14847  prodfrec  14848  ntrivcvg  14850  prodmo  14887  fprodss  14899  fprodabs  14925  fprodn0  14930  fprod2d  14932  fprodefsum  15045  ruclem8  15186  ruclem9  15187  dvdsmod0  15209  dvds2ln  15237  dvdsaddre2b  15252  dvdslelem  15254  dvdsdivcl  15261  alzdvds  15265  mod2eq1n2dvds  15291  oddnn02np1  15292  nn0o1gt2  15317  nno  15318  sumeven  15330  sumodd  15331  pwp1fsum  15334  ndvdsadd  15353  bitsinv1  15383  sadcadd  15399  sadadd2  15401  saddisjlem  15405  smuval2  15423  smupvallem  15424  smu01lem  15426  smupval  15429  smueqlem  15431  smumullem  15433  gcddiv  15487  gcdmultiple  15488  rplpwr  15495  nn0seqcvgd  15502  seq1st  15503  alginv  15507  algcvga  15511  algfx  15512  absprodnn  15550  isprm2  15613  isprm3  15614  prmind2  15616  maxprmfct  15638  prmdvdsexp  15644  pcmpt  15813  prmreclem4  15840  vdwmc2  15900  vdwlem10  15911  ramub2  15935  ramcl  15950  prmgaplem5  15976  prmgaplem8  15979  cshwshashlem1  16014  cshwshashlem3  16016  setsn0fun  16106  imasleval  16406  divsfval  16412  mreexexlem4d  16512  isssc  16684  initoeu1  16865  termoeu1  16872  istos  17240  mgmcl  17450  frmdgsum  17604  dfgrp3lem  17718  mhmmulg  17785  resghm2b  17880  gsumwrev  17997  elsymgbas  18003  symgextf1  18042  gsmsymgreqlem2  18052  gsmsymgreq  18053  odlem1  18155  odcl2  18183  gexlem1  18195  efgi2  18339  efginvrel2  18341  efgsrel  18348  cyggexb  18501  gsummulglem  18542  gsumzunsnd  18556  gsum2dlem2  18571  telgsums  18592  dmdprd  18599  dprdw  18611  ablfac1eulem  18673  srgpcomp  18734  lmodfopnelem1  19103  rmodislmodlem  19134  mplcoe1  19674  mplcoe3  19675  mplcoe5  19677  cply1mul  19872  coe1fzgsumdlem  19879  gsummoncoe1  19882  pf1ind  19927  evl1gsumdlem  19928  cnfldmulg  19986  cnfldexp  19987  obslbs  20284  mat1dimcrng  20494  ma1repveval  20588  mulmarep1gsum2  20591  gsummatr01lem3  20675  cramerlem3  20708  decpmatmulsumfsupp  20791  mp2pm2mplem4  20827  pm2mpmhmlem1  20836  fvmptnn04if  20867  cayhamlem1  20884  fctop  21022  mretopd  21110  restopnb  21193  restdis  21196  tgcnp  21271  cncls2  21291  cncls  21292  cnntr  21293  cnsscnp  21297  cmpsub  21417  2ndcsep  21476  1stcelcls  21478  lfinpfin  21541  locfincmp  21543  comppfsc  21549  txcn  21643  txlm  21665  xkohaus  21670  qtopres  21715  haushmphlem  21804  cmphmph  21805  connhmph  21806  reghmph  21810  nrmhmph  21811  ptcmpfi  21830  reghaus  21842  fbssfi  21854  fbun  21857  fbfinnfr  21858  isfildlem  21874  fgcl  21895  cfinfil  21910  supfil  21912  ufinffr  21946  fin1aufil  21949  cnpflf  22018  alexsubALTlem3  22066  alexsubALT  22068  cnextfvval  22082  cnextcn  22084  tmdmulg  22109  tmdgsum  22112  tgphaus  22133  tgpt1  22134  mettri  22370  blssexps  22444  blssex  22445  mopni3  22512  metss  22526  psmetutop  22585  dscmet  22590  tngngp3  22673  rectbntr0  22848  metnrmlem1a  22874  fsumcn  22886  lmmbr  23268  caubl  23318  caublcls  23319  bcthlem5  23337  bcth3  23340  ovolunlem1a  23477  ovoliunnul  23488  finiunmbl  23525  voliunlem1  23531  volsuplem  23536  volsup  23537  dyadmax  23579  itgfsum  23807  dvnadd  23906  cpnord  23912  dvnfre  23929  dvmptfsum  23952  dvlip  23970  fta1g  24141  plyco  24211  dgrcolem1  24243  dgrco  24245  dvnply2  24256  plydivex  24266  plyexmo  24282  aannenlem1  24297  aaliou3lem2  24312  dvntaylp  24339  taylthlem1  24341  ulmval  24348  cxpmul2  24649  scvxcvx  24926  jensenlem2  24928  jensen  24929  ppiub  25143  bcmono  25216  bpos1lem  25221  bposlem5  25227  gausslemma2dlem6  25311  lgsquad2lem2  25324  2lgslem3  25343  2lgs  25346  dchrisumlem1  25392  dchrisum0flb  25413  pntpbnd1  25489  pntlemf  25508  qabvle  25528  qabvexp  25529  ostthlem2  25531  ostth2lem2  25537  axeuclidlem  26056  axcontlem12  26069  umgrnloopv  26215  uhgredgrnv  26239  edglnl  26253  numedglnl  26254  usgruspgrb  26291  usgrnloopvALT  26308  usgredg2vlem2  26333  subupgr  26395  nbumgr  26459  uhgrnbgr0nb  26466  nbgr0vtxlem  26467  edgusgrnbfin  26491  nb3grprlem2  26499  uvtxnbgrvtx  26513  cplgrop  26561  cusgrfi  26582  fusgrmaxsize  26588  fusgrn0degnn0  26623  ewlkprop  26727  uspgr2wlkeq  26770  g0wlk0  26776  wlkreslem  26794  wlkres  26795  lfgriswlk  26813  upgrwlkdvde  26861  spthonepeq  26876  uhgrwkspth  26879  usgr2trlncl  26884  usgr2trlspth  26885  cyclnspth  26924  crctcshwlkn0lem3  26933  wwlksn  26958  wspthneq1eq2  26987  wwlksm1edg  27008  wwlksnred  27029  wwlksnextfun  27035  wwlksnextinj  27036  wwlksnextproplem3  27049  wspthsnonn0vne  27057  wspn0  27064  rusgrnumwwlk  27117  clwwlkccatlem  27132  umgrclwwlkge2  27134  clwlkclwwlklem2  27143  clwlkclwwlklem3  27144  clwwisshclwws  27158  clwwisshclwwsn  27159  clwwlknOLD  27172  clwwlkn1loopb  27192  clwwlknfi  27194  wwlksext2clwwlk  27207  wwlksubclwwlk  27209  clwlksfclwwlkOLD  27236  clwwlknonwwlknonb  27274  clwwlknonex2lem2  27277  upgr3v3e3cycl  27353  uhgr3cyclex  27355  upgr4cycl4dv4e  27358  eupthseg  27379  upgreupthseg  27382  eupth2lem3lem4  27404  eupth2lem3lem7  27407  eupth2  27412  eulerpath  27414  nfrgr2v  27447  frgr3vlem1  27448  3vfriswmgr  27453  1to2vfriswmgr  27454  1to3vfriswmgr  27455  3cyclfrgrrn1  27460  3cyclfrgrrn  27461  3cyclfrgrrn2  27462  4cycl2vnunb  27465  frgrncvvdeqlem2  27475  frgrncvvdeqlem8  27481  frgrncvvdeqlem9  27482  frgrwopreglem4a  27485  frgrwopreglem5lem  27495  frgrwopreglem5ALT  27497  frgrregorufr0  27499  frgr2wwlk1  27504  frgr2wwlkeqm  27506  fusgr2wsp2nb  27509  2wspmdisj  27512  frrusgrord  27516  numclwwlk1lem2f1  27536  numclwlk1  27551  frgrreggt1  27581  friendshipgt3  27586  hlim2  28377  elnlfn  29115  stle0i  29426  hstrbi  29453  spansncv2  29480  h1da  29536  fmptcof2  29784  nnindd  29893  xreceu  29955  tpr2rico  30283  hasheuni  30472  ismeas  30587  sseqp1  30782  rrvsum  30841  dstfrvunirn  30861  sgn3da  30928  bnj607  31309  bnj1145  31384  bnj1204  31403  subfacp1lem6  31490  cvmlift2lem12  31619  cvmlift3lem4  31627  mrsubvrs  31742  climuzcnv  31887  iprodefisumlem  31948  fprb  31991  dfon2lem9  32016  trpredtr  32050  trpredmintr  32051  dftrpred3g  32053  trpredrec  32058  soseq  32075  sltval2  32130  sltsolem1  32147  linethru  32581  elhf2  32603  finminlem  32633  fnessref  32673  neibastop2lem  32676  fnemeet2  32683  nndivsub  32773  bj-cbval2v  33051  bj-xpnzex  33256  bj-intss  33364  mptsnunlem  33502  dissneqlem  33504  topdifinffinlem  33511  iooelexlt  33526  wl-exeq  33635  wl-ax11-lem3  33678  matunitlindflem1  33718  poimirlem22  33744  poimirlem26  33748  poimirlem28  33750  poimirlem29  33751  poimirlem32  33754  heicant  33757  ovoliunnfl  33764  voliunnfl  33766  volsupnfl  33767  cover2  33820  upixp  33836  sdclem2  33849  fdc  33852  seqpo  33854  metf1o  33862  mettrifi  33864  sstotbnd3  33886  heibor1lem  33919  heiborlem5  33925  heibor  33931  bfplem1  33932  elghomlem2OLD  33996  grpokerinj  34003  isrngo  34007  rngodm1dm2  34042  ispridl2  34148  exlimddvf  34236  lssatle  34795  4atexlemex4  35853  mzpsubst  37813  jm2.18  38056  wepwsolem  38113  iunrelexp0  38494  relexpmulg  38502  cnvtrclfv  38516  clsk1indlem3  38841  dvgrat  39011  radcnvrat  39013  sbcoreleleqVD  39589  csbxpgVD  39624  sineq0ALT  39667  islptre  40331  iblspltprt  40668  stoweidlem2  40698  stoweidlem17  40713  stoweidlem21  40717  2reu2  41699  afveu  41742  funbrafv  41747  ndmaovass  41795  afv2eu  41827  tz6.12c-afv2  41831  funop1  41873  f1oresf1o2  41881  fvmptrabdm  41883  nltle2tri  41898  2elfz2melfz  41903  fzoopth  41912  fsummsndifre  41917  fsumsplitsndif  41918  fsummmodsndifre  41919  fsummmodsnunz  41920  iccpartimp  41928  iccpartiltu  41933  iccpartigtl  41934  iccpartleu  41939  iccpartgel  41940  iccpartrn  41941  iccpartiun  41945  icceuelpart  41947  iccpartnel  41949  fargshiftf  41951  fargshiftf1  41952  pfxccatin12lem2  41999  pfxccat3  42001  fmtnoinf  42023  odz2prm2pw  42050  lighneallem4  42102  lighneal  42103  evensumeven  42191  even3prm2  42203  gbowgt5  42225  nnsum4primeseven  42263  nnsum4primesevenALTV  42264  bgoldbnnsum3prm  42267  bgoldbtbndlem2  42269  bgoldbtbndlem4  42271  bgoldbtbnd  42272  elsprel  42293  prsprel  42305  sprsymrelfo  42315  clcllaw  42395  nrhmzr  42441  rnghmmul  42468  rngccatidALTV  42557  ringccatidALTV  42620  nzerooringczr  42640  scmsuppss  42721  gsumlsscl  42732  ply1mulgsumlem2  42743  lincvalsc0  42778  linc0scn0  42780  lincdifsn  42781  linc1  42782  lincellss  42783  lincsum  42786  lincscm  42787  lincsumcl  42788  lcoss  42793  lincext3  42813  lindslinindimp2lem4  42818  lindslinindsimp2lem5  42819  lindslinindsimp2  42820  lindsrng01  42825  snlindsntor  42828  lincresunit3lem2  42837  lincresunit3  42838  islindeps2  42840  blengt1fldiv2p1  42955