Theorem expcom 413

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 412	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3	2	com12 32	1 ⊢ (𝜓 → (𝜑 → 𝜒))

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  ancoms  458  pm3.21  471  sylan  580  animpimp2impd  846  4casesdan  1041  dedlema  1045  dedlemb  1046  sbiedvw  2100  mo4  2566  2moswapv  2629  2moswap  2644  2mosOLD  2650  2eu2  2653  pm2.61ne  3017  nelelne  3031  r19.21be  3229  cbvraldva2  3318  rspcebdv  3570  2reu2  3848  csbie2df  4395  minel  4418  uneqdifeq  4445  raltpd  4738  ssunsn2  4783  opthprneg  4821  ssuni  4888  uniss2  4897  elpwuni  5060  intss2  5063  disjord  5087  elpw2g  5278  elssabg  5288  axprlem3OLD  5373  axprlem4OLD  5374  axprlem5OLD  5375  oteqex  5448  otsndisj  5467  otiunsndisj  5468  epelg  5525  wereu  5620  relop  5799  riinint  5921  sotri3  6087  unixpid  6242  reuop  6251  ordtr2  6362  ordsssuc2  6410  iotan0  6482  funopg  6526  fun  6696  fvmptnf  6963  fvn0ssdmfun  7019  eldmrexrnb  7037  fmptco  7074  fnressn  7103  fressnfv  7105  fprb  7140  fvtp2g  7145  fvtp3g  7146  fconst2g  7149  fntpb  7155  f1dom3el3dif  7215  f1ounsn  7218  isores3  7281  isoselem  7287  oprabv  7418  eloprabga  7467  sorpsscmpl  7679  difex2  7705  ordpwsuc  7757  ordsucun  7767  limuni3  7794  trom  7817  fo1stres  7959  poxp  8070  soxp  8071  xpord3inddlem  8096  soseq  8101  suppimacnv  8116  fsuppeq  8117  funsssuppss  8132  brtpos2  8174  frrlem8  8235  fpr2a  8244  onnseq  8276  smores  8284  smofvon2  8288  tfrlem1  8307  oacl  8462  omcl  8463  oecl  8464  oawordri  8477  oalimcl  8487  oaass  8488  oarec  8489  omwordri  8499  omeulem1  8509  omeulem2  8510  oeordi  8515  oeworde  8521  oeoelem  8526  nnacl  8539  nnmcl  8540  nnecl  8541  nnacom  8545  nnaass  8550  nnmsucr  8553  nnmordi  8559  omabs  8579  cofonr  8602  naddunif  8621  iiner  8726  elpmg  8780  fsetfcdm  8797  fsetprcnex  8799  pmss12g  8807  mapfvd  8817  f1domg  8908  ssdomg  8937  undom  8993  domtriord  9051  ssnnfi  9094  fnfi  9102  enfi  9111  php  9131  sdom1  9150  1sdom2dom  9154  fisseneq  9163  isinf  9165  dif1ennnALT  9177  findcard3  9183  frfi  9185  difinf  9211  imafiOLD  9216  iunfi  9243  fsuppunfi  9291  fsuppres  9296  ffsuppbi  9301  elfi2  9317  marypha1lem  9336  marypha1  9337  oiexg  9440  wemapso2  9458  harword  9468  brwdom  9472  unxpwdom  9494  en3lplem1  9521  inf3lemd  9536  inf3lem5  9541  cantnfval2  9578  cantnfle  9580  cantnflt  9581  cnfcom  9609  tcmin  9648  frr2  9672  r1sdom  9686  rankxplim3  9793  cardidm  9871  cardmin2  9911  infxpenlem  9923  fseqenlem1  9934  numacn  9959  alephordi  9984  iscard3  10003  alephinit  10005  carduniima  10006  iunfictbso  10024  dfac5  10039  dfac12lem3  10056  nnadju  10108  pwsdompw  10113  pwdjudom  10125  cflim2  10173  cfslb2n  10178  cofsmo  10179  cfsmolem  10180  cfcoflem  10182  alephsing  10186  infpssALT  10223  fin23lem34  10256  isf32lem2  10264  isf32lem10  10272  isf32lem12  10274  isfin1-2  10295  hsmexlem4  10339  axcc2lem  10346  domtriomlem  10352  axdc2lem  10358  axdc3lem2  10361  axdc3lem4  10363  axdc4lem  10365  axcclem  10367  ac6num  10389  ac6s  10394  zorn2lem7  10412  ttukeylem5  10423  imadomg  10444  iundom2g  10450  ondomon  10473  ficard  10475  konigthlem  10479  alephreg  10493  pwcfsdom  10494  cfpwsdom  10495  axregndlem1  10513  axregnd  10515  pwfseqlem3  10571  pwxpndom2  10576  pwxpndom  10577  pwdjundom  10578  inawinalem  10600  gchina  10610  wuncval2  10658  tsk0  10674  tskxpss  10683  inatsk  10689  tskuni  10694  gruina  10729  grothac  10741  addclpi  10803  addnidpi  10812  nqereu  10840  mulcanenq  10871  genpnnp  10916  nqpr  10925  prlem934  10944  reclem2pr  10959  suplem1pr  10963  supsrlem  11022  axpre-sup  11080  1re  11132  dedekindle  11297  00id  11308  receu  11782  sup3  12099  infrelb  12127  peano5nni  12148  nnindd  12165  nnaddcl  12168  zrevaddcl  12536  nzadd  12539  zdiv  12562  nneo  12576  zeo2  12579  nn0indd  12589  fzind  12590  fnn0ind  12591  fzindd  12594  uzwo  12824  lbzbi  12849  nn01to3  12854  qrevaddcl  12884  irradd  12886  irrmul  12887  ltsubrp  12943  ltaddrp  12944  xnn0xaddcl  13150  xnn0xadd0  13162  icoshft  13389  fzen  13457  elfzm11  13511  uzsplit  13512  elfzom1elp1fzo  13648  fzoopth  13678  injresinjlem  13706  injresinj  13707  modifeq2int  13856  modsumfzodifsn  13867  om2uzlti  13873  ssnn0fi  13908  fsuppmapnn0fiub0  13916  mptnn0fsuppr  13922  seqcaopr3  13960  seqf1olem2a  13963  seqf1o  13966  ser1const  13981  expadd  14027  expmul  14030  leexp1a  14098  faccl  14206  facdiv  14210  faclbnd  14213  faclbnd4lem4  14219  hasheqf1oi  14274  hashgadd  14300  hashinfxadd  14308  hashunx  14309  hashunsng  14315  elprchashprn2  14319  hashss  14332  hash1snb  14342  hashmap  14358  hashf1lem2  14379  hashf1  14380  seqcoll  14387  hashle2pr  14400  hashdmpropge2  14406  hashge3el3dif  14410  hash1to3  14415  fundmge2nop0  14425  fi1uzind  14430  brfi1indALT  14433  sswrd  14445  swrdnd2  14579  swrdnnn0nd  14580  swrdnd0  14581  swrdwrdsymb  14586  pfxnd0  14612  swrdswrdlem  14627  swrdswrd  14628  wrd2ind  14646  swrdccatin1  14648  swrdccatin2  14652  pfxccatin12lem2  14654  pfxccat3  14657  repsdf2  14701  repswswrd  14707  cshw0  14717  cshwcl  14721  cshwlen  14722  cshf1  14733  swrdco  14760  relexpsucnnl  14953  rtrclreclem3  14983  rtrclreclem4  14984  relexpindlem  14986  rtrclind  14988  shftlem  14991  caubnd  15282  reusq0  15388  rlimcld2  15501  o1dif  15553  climub  15585  climserle  15586  iseraltlem2  15606  sumss  15647  fsumzcl2  15662  fsummsnunz  15677  fsumsplitsnun  15678  fsum2d  15694  modfsummods  15716  fsumabs  15724  fsumrlim  15734  fsumo1  15735  fsumiun  15744  climcndslem1  15772  climcndslem2  15773  cvgrat  15806  clim2prod  15811  prodfn0  15817  prodfrec  15818  ntrivcvg  15820  prodmo  15859  fprodss  15871  fprodabs  15897  fprodn0  15902  fprod2d  15904  fprodefsum  16018  ruclem8  16162  ruclem9  16163  dvdsmod0  16185  dvds2ln  16216  dvdsaddre2b  16234  dvdslelem  16236  dvdsdivcl  16243  alzdvds  16247  mod2eq1n2dvds  16274  oddnn02np1  16275  nn0o1gt2  16308  nno  16309  sumeven  16314  sumodd  16315  pwp1fsum  16318  ndvdsadd  16337  bitsinv1  16369  sadcadd  16385  sadadd2  16387  saddisjlem  16391  smuval2  16409  smupvallem  16410  smu01lem  16412  smupval  16415  smueqlem  16417  smumullem  16419  gcddiv  16478  rplpwr  16485  nn0seqcvgd  16497  seq1st  16498  alginv  16502  algcvga  16506  algfx  16507  absprodnn  16545  isprm2  16609  isprm3  16610  prmind2  16612  maxprmfct  16636  prmdvdsexp  16642  pcmpt  16820  prmreclem4  16847  vdwmc2  16907  vdwlem10  16918  ramub2  16942  ramcl  16957  prmgaplem5  16983  prmgaplem8  16986  cshwshashlem1  17023  cshwshashlem3  17025  setsn0fun  17100  imasleval  17462  divsfval  17468  mreexexlem4d  17570  isssc  17744  initoeu1  17935  termoeu1  17942  istos  18339  chnfibg  18559  mgmcl  18568  sgrpidmnd  18664  frmdgsum  18787  smndex1mgm  18832  dfgrp3lem  18968  mhmmulg  19045  resghm2b  19163  gsumwrev  19295  elsymgbas  19303  symgextf1  19350  gsmsymgreqlem2  19360  gsmsymgreq  19361  odlem1  19464  odcl2  19494  gexlem1  19508  efgi2  19654  efginvrel2  19656  efgsrel  19663  cyggexb  19828  gsummulglem  19870  gsumzunsnd  19885  gsum2dlem2  19900  telgsums  19922  dmdprd  19929  dprdw  19941  ablfac1eulem  20003  srgpcomp  20153  rnghmmul  20385  nrhmzr  20470  lmodfopnelem1  20849  rmodislmodlem  20880  cnfldmulg  21358  cnfldexp  21359  nzerooringczr  21435  obslbs  21685  mplcoe1  21992  mplcoe3  21993  mplcoe5  21995  cply1mul  22240  coe1fzgsumdlem  22247  gsummoncoe1  22252  pf1ind  22299  evl1gsumdlem  22300  mat1dimcrng  22421  ma1repveval  22515  mulmarep1gsum2  22518  gsummatr01lem3  22601  cramerlem3  22633  decpmatmulsumfsupp  22717  mp2pm2mplem4  22753  pm2mpmhmlem1  22762  fvmptnn04if  22793  cayhamlem1  22810  fctop  22948  mretopd  23036  restopnb  23119  restdis  23122  tgcnp  23197  cncls2  23217  cncls  23218  cnntr  23219  cnsscnp  23223  cmpsub  23344  2ndcsep  23403  1stcelcls  23405  lfinpfin  23468  locfincmp  23470  comppfsc  23476  txcn  23570  txlm  23592  xkohaus  23597  qtopres  23642  haushmphlem  23731  cmphmph  23732  connhmph  23733  reghmph  23737  nrmhmph  23738  ptcmpfi  23757  reghaus  23769  fbssfi  23781  fbun  23784  fbfinnfr  23785  isfildlem  23801  fgcl  23822  cfinfil  23837  supfil  23839  ufinffr  23873  fin1aufil  23876  cnpflf  23945  alexsubALTlem3  23993  alexsubALT  23995  cnextfvval  24009  cnextcn  24011  tmdgsum  24039  tgphaus  24061  tgpt1  24062  mettri  24296  blssexps  24370  blssex  24371  mopni3  24438  metss  24452  psmetutop  24511  dscmet  24516  tngngp3  24600  rectbntr0  24777  metnrmlem1a  24803  fsumcn  24817  lmmbr  25214  caubl  25264  caublcls  25265  bcthlem5  25284  bcth3  25287  ovolunlem1a  25453  ovoliunnul  25464  finiunmbl  25501  voliunlem1  25507  volsuplem  25512  volsup  25513  dyadmax  25555  itgfsum  25784  dvnadd  25887  cpnord  25893  dvnfre  25912  dvmptfsum  25935  dvlip  25954  fta1g  26131  plyco  26202  dgrcolem1  26235  dgrco  26237  dvnply2  26251  plydivex  26261  plyexmo  26277  aannenlem1  26292  aaliou3lem2  26307  dvntaylp  26335  taylthlem1  26337  ulmval  26345  cxpmul2  26654  cxpsqrtth  26695  scvxcvx  26952  jensenlem2  26954  jensen  26955  ppiub  27171  bcmono  27244  bpos1lem  27249  bposlem5  27255  gausslemma2dlem6  27339  lgsquad2lem2  27352  2lgslem3  27371  2lgs  27374  2sqnn  27406  addsqnreup  27410  2sqreultblem  27415  2sqreunnltblem  27418  dchrisumlem1  27456  dchrisum0flb  27477  pntpbnd1  27553  pntlemf  27572  qabvle  27592  qabvexp  27593  ostthlem2  27595  ostth2lem2  27601  ltsval2  27624  ltssolem1  27643  negsprop  28031  mulsuniflem  28145  precsexlem6  28208  precsexlem7  28209  noseqind  28288  om2noseqlt  28295  n0addscl  28340  n0mulscl  28341  expsne0  28432  axeuclidlem  29035  axcontlem12  29048  umgrnloopv  29179  uhgredgrnv  29203  edglnl  29216  numedglnl  29217  usgruspgrb  29256  usgrnloopvALT  29274  usgredg2vlem2  29299  subupgr  29360  nbumgr  29420  uhgrnbgr0nb  29427  nbgr0edglem  29429  edgusgrnbfin  29446  nb3grprlem2  29454  uvtxnbgrvtx  29466  cplgrop  29510  cusgrfi  29532  fusgrmaxsize  29538  fusgrn0degnn0  29573  ewlkprop  29677  uspgr2wlkeq  29719  g0wlk0  29724  wlkreslem  29741  lfgriswlk  29760  upgrwlkdvde  29810  spthonepeq  29825  uhgrwkspth  29828  usgr2trlncl  29833  usgr2trlspth  29834  cyclnumvtx  29873  cyclnspth  29874  crctcshwlkn0lem3  29885  wwlksn  29910  wspthneq1eq2  29933  wwlksm1edg  29954  wwlksnred  29965  wwlksnextfun  29971  wwlksnextinj  29972  wwlksnextproplem3  29984  wspthsnonn0vne  29990  wspn0  29997  rusgrnumwwlk  30051  clwwlkccatlem  30064  umgrclwwlkge2  30066  clwlkclwwlklem2  30075  clwlkclwwlklem3  30076  clwwisshclwws  30090  clwwisshclwwsn  30091  clwwlkn1loopb  30118  wwlksext2clwwlk  30132  wwlksubclwwlk  30133  clwwlknonex2lem2  30183  upgr3v3e3cycl  30255  uhgr3cyclex  30257  upgr4cycl4dv4e  30260  eupth2lem3lem4  30306  eupth2lem3lem7  30309  eupth2  30314  eulerpath  30316  nfrgr2v  30347  frgr3vlem1  30348  3vfriswmgr  30353  1to2vfriswmgr  30354  1to3vfriswmgr  30355  3cyclfrgrrn1  30360  3cyclfrgrrn  30361  3cyclfrgrrn2  30362  4cycl2vnunb  30365  frgrncvvdeqlem2  30375  frgrncvvdeqlem8  30381  frgrncvvdeqlem9  30382  frgrwopreglem4a  30385  frgrwopreglem5lem  30395  frgrwopreglem5ALT  30397  frgrregorufr0  30399  frgr2wwlk1  30404  frgr2wwlkeqm  30406  fusgr2wsp2nb  30409  2wspmdisj  30412  frrusgrord  30416  numclwwlk1lem2f1  30432  numclwlk1  30446  frgrreggt1  30468  friendshipgt3  30473  hlim2  31267  elnlfn  32003  stle0i  32314  hstrbi  32341  spansncv2  32368  h1da  32424  fmptcof2  32735  sgn3da  32915  xreceu  33003  domnprodn0  33357  1arithufdlem3  33627  1arithufdlem4  33628  tpr2rico  34069  hasheuni  34242  ismeas  34356  sseqp1  34552  rrvsum  34611  dstfrvunirn  34632  signstfvc  34731  bnj607  35072  bnj1145  35149  bnj1204  35168  r1filim  35260  fineqvrep  35270  fineqvnttrclselem1  35277  onvf1odlem4  35300  fisshasheq  35309  subgrwlk  35326  subfacp1lem6  35379  cvmlift2lem12  35508  cvmlift3lem4  35516  satfrnmapom  35564  sat1el2xp  35573  satffunlem2  35602  satffun  35603  mrsubvrs  35716  climuzcnv  35865  iprodefisumlem  35934  dfon2lem9  35983  linethru  36347  elhf2  36369  finminlem  36512  fnessref  36551  neibastop2lem  36554  fnemeet2  36561  nndivsub  36651  bj-xpnzex  37160  bj-elpwg  37253  bj-epelg  37269  mptsnunlem  37539  dissneqlem  37541  topdifinffinlem  37548  iooelexlt  37563  domalom  37605  fvineqsneq  37613  wl-exeq  37735  matunitlindflem1  37813  poimirlem22  37839  poimirlem26  37843  poimirlem28  37845  poimirlem29  37846  poimirlem32  37849  heicant  37852  ovoliunnfl  37859  voliunnfl  37861  volsupnfl  37862  cover2  37912  upixp  37926  sdclem2  37939  fdc  37942  seqpo  37944  metf1o  37952  mettrifi  37954  sstotbnd3  37973  heibor1lem  38006  heiborlem5  38012  heibor  38018  bfplem1  38019  elghomlem2OLD  38083  grpokerinj  38090  isrngo  38094  rngodm1dm2  38129  ispridl2  38235  exlimddvf  38318  lssatle  39271  4atexlemex4  40329  uzindd  42227  evl1gprodd  42367  sn-axprlem3  42470  redvmptabs  42611  sn-sup3d  42743  mzpsubst  42986  jm2.18  43226  wepwsolem  43280  oaabsb  43532  oacl2g  43568  ofoafg  43592  ofoaid1  43596  ofoaid2  43597  naddonnn  43633  iunrelexp0  43939  relexpmulg  43947  cnvtrclfv  43961  clsk1indlem3  44280  grucollcld  44497  inaex  44534  dvgrat  44549  radcnvrat  44551  csbxpgVD  45130  sineq0ALT  45173  trfr  45199  relwf  45204  pwclaxpow  45221  omssaxinf2  45225  islptre  45861  iblspltprt  46213  stoweidlem2  46242  stoweidlem17  46257  stoweidlem21  46261  2reuimp0  47356  2reuimp  47357  afveu  47395  funbrafv  47400  ndmaovass  47448  afv2eu  47480  tz6.12c-afv2  47484  funop1  47525  f1oresf1o2  47533  fvmptrabdm  47535  nltle2tri  47555  2elfz2melfz  47560  fsummsndifre  47614  fsumsplitsndif  47615  fsummmodsndifre  47616  fsummmodsnunz  47617  elsetpreimafvssdm  47628  uniimaelsetpreimafv  47638  imasetpreimafvbijlemfv1  47645  iccpartiltu  47664  iccpartigtl  47665  iccpartleu  47670  iccpartgel  47671  iccpartrn  47672  iccpartiun  47676  icceuelpart  47678  iccpartnel  47680  fargshiftf  47682  fargshiftf1  47683  ichnfb  47707  elsprel  47717  prsprel  47729  sprsymrelfo  47739  paireqne  47753  sbcpr  47763  reupr  47764  fmtnoinf  47778  odz2prm2pw  47805  lighneallem4  47852  lighneal  47853  requad1  47864  requad2  47865  evensumeven  47949  even3prm2  47961  gbowgt5  48004  nnsum4primeseven  48042  nnsum4primesevenALTV  48043  bgoldbnnsum3prm  48046  bgoldbtbndlem2  48048  bgoldbtbndlem4  48050  bgoldbtbnd  48051  dfsclnbgr6  48100  grimco  48131  cycl3grtri  48189  isubgr3stgrlem6  48213  gricgrlic  48260  gpgedgvtx0  48303  gpgprismgr4cycllem3  48339  pgnbgreunbgrlem5  48365  clcllaw  48433  rngccatidALTV  48514  ringccatidALTV  48548  scmsuppss  48613  gsumlsscl  48622  ply1mulgsumlem2  48629  lincvalsc0  48663  linc0scn0  48665  lincdifsn  48666  linc1  48667  lincellss  48668  lincsum  48671  lincscm  48672  lincsumcl  48673  lcoss  48678  lincext3  48698  lindslinindimp2lem4  48703  lindslinindsimp2lem5  48704  lindslinindsimp2  48705  lindsrng01  48710  snlindsntor  48713  lincresunit3lem2  48722  lincresunit3  48723  islindeps2  48725  blengt1fldiv2p1  48835  2arymaptf1  48895  resum2sqorgt0  48951  reorelicc  48952  rrx2plordisom  48965  rrx2linest  48984  rrxsphere  48990  line2ylem  48993  itsclc0xyqsol  49010  itscnhlinecirc02p  49027  mo0sn  49057  thincn0eu  49672