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  2563  2moswapv  2626  2moswap  2641  2mosOLD  2647  2eu2  2650  pm2.61ne  3014  nelelne  3028  r19.21be  3226  cbvraldva2  3315  rspcebdv  3567  2reu2  3845  csbie2df  4392  minel  4415  uneqdifeq  4442  raltpd  4733  ssunsn2  4778  opthprneg  4816  ssuni  4883  uniss2  4892  elpwuni  5055  intss2  5058  disjord  5082  elpw2g  5273  elssabg  5283  axprlem3OLD  5368  axprlem4OLD  5369  axprlem5OLD  5370  oteqex  5443  otsndisj  5462  otiunsndisj  5463  epelg  5520  wereu  5615  relop  5794  riinint  5915  sotri3  6081  unixpid  6236  reuop  6245  ordtr2  6356  ordsssuc2  6404  iotan0  6476  funopg  6520  fun  6690  fvmptnf  6957  fvn0ssdmfun  7013  eldmrexrnb  7031  fmptco  7068  fnressn  7097  fressnfv  7099  fprb  7134  fvtp2g  7139  fvtp3g  7140  fconst2g  7143  fntpb  7149  f1dom3el3dif  7209  f1ounsn  7212  isores3  7275  isoselem  7281  oprabv  7412  eloprabga  7461  sorpsscmpl  7673  difex2  7699  ordpwsuc  7751  ordsucun  7761  limuni3  7788  trom  7811  fo1stres  7953  poxp  8064  soxp  8065  xpord3inddlem  8090  soseq  8095  suppimacnv  8110  fsuppeq  8111  funsssuppss  8126  brtpos2  8168  frrlem8  8229  fpr2a  8238  onnseq  8270  smores  8278  smofvon2  8282  tfrlem1  8301  oacl  8456  omcl  8457  oecl  8458  oawordri  8471  oalimcl  8481  oaass  8482  oarec  8483  omwordri  8493  omeulem1  8503  omeulem2  8504  oeordi  8508  oeworde  8514  oeoelem  8519  nnacl  8532  nnmcl  8533  nnecl  8534  nnacom  8538  nnaass  8543  nnmsucr  8546  nnmordi  8552  omabs  8572  cofonr  8595  naddunif  8614  iiner  8719  elpmg  8773  fsetfcdm  8790  fsetprcnex  8792  pmss12g  8799  mapfvd  8809  f1domg  8900  ssdomg  8929  undom  8985  domtriord  9043  ssnnfi  9086  fnfi  9094  enfi  9103  php  9123  sdom1  9141  1sdom2dom  9145  fisseneq  9154  isinf  9156  dif1ennnALT  9168  findcard3  9174  frfi  9176  difinf  9202  imafiOLD  9207  iunfi  9234  fsuppunfi  9279  fsuppres  9284  ffsuppbi  9289  elfi2  9305  marypha1lem  9324  marypha1  9325  oiexg  9428  wemapso2  9446  harword  9456  brwdom  9460  unxpwdom  9482  en3lplem1  9509  inf3lemd  9524  inf3lem5  9529  cantnfval2  9566  cantnfle  9568  cantnflt  9569  cnfcom  9597  tcmin  9636  frr2  9660  r1sdom  9674  rankxplim3  9781  cardidm  9859  cardmin2  9899  infxpenlem  9911  fseqenlem1  9922  numacn  9947  alephordi  9972  iscard3  9991  alephinit  9993  carduniima  9994  iunfictbso  10012  dfac5  10027  dfac12lem3  10044  nnadju  10096  pwsdompw  10101  pwdjudom  10113  cflim2  10161  cfslb2n  10166  cofsmo  10167  cfsmolem  10168  cfcoflem  10170  alephsing  10174  infpssALT  10211  fin23lem34  10244  isf32lem2  10252  isf32lem10  10260  isf32lem12  10262  isfin1-2  10283  hsmexlem4  10327  axcc2lem  10334  domtriomlem  10340  axdc2lem  10346  axdc3lem2  10349  axdc3lem4  10351  axdc4lem  10353  axcclem  10355  ac6num  10377  ac6s  10382  zorn2lem7  10400  ttukeylem5  10411  imadomg  10432  iundom2g  10438  ondomon  10461  ficard  10463  konigthlem  10466  alephreg  10480  pwcfsdom  10481  cfpwsdom  10482  axregndlem1  10500  axregnd  10502  pwfseqlem3  10558  pwxpndom2  10563  pwxpndom  10564  pwdjundom  10565  inawinalem  10587  gchina  10597  wuncval2  10645  tsk0  10661  tskxpss  10670  inatsk  10676  tskuni  10681  gruina  10716  grothac  10728  addclpi  10790  addnidpi  10799  nqereu  10827  mulcanenq  10858  genpnnp  10903  nqpr  10912  prlem934  10931  reclem2pr  10946  suplem1pr  10950  supsrlem  11009  axpre-sup  11067  1re  11119  dedekindle  11284  00id  11295  receu  11769  sup3  12086  infrelb  12114  peano5nni  12135  nnindd  12152  nnaddcl  12155  zrevaddcl  12523  nzadd  12526  zdiv  12549  nneo  12563  zeo2  12566  nn0indd  12576  fzind  12577  fnn0ind  12578  fzindd  12581  uzwo  12811  lbzbi  12836  nn01to3  12841  qrevaddcl  12871  irradd  12873  irrmul  12874  ltsubrp  12930  ltaddrp  12931  xnn0xaddcl  13136  xnn0xadd0  13148  icoshft  13375  fzen  13443  elfzm11  13497  uzsplit  13498  elfzom1elp1fzo  13634  fzoopth  13664  injresinjlem  13692  injresinj  13693  modifeq2int  13842  modsumfzodifsn  13853  om2uzlti  13859  ssnn0fi  13894  fsuppmapnn0fiub0  13902  mptnn0fsuppr  13908  seqcaopr3  13946  seqf1olem2a  13949  seqf1o  13952  ser1const  13967  expadd  14013  expmul  14016  leexp1a  14084  faccl  14192  facdiv  14196  faclbnd  14199  faclbnd4lem4  14205  hasheqf1oi  14260  hashgadd  14286  hashinfxadd  14294  hashunx  14295  hashunsng  14301  elprchashprn2  14305  hashss  14318  hash1snb  14328  hashmap  14344  hashf1lem2  14365  hashf1  14366  seqcoll  14373  hashle2pr  14386  hashdmpropge2  14392  hashge3el3dif  14396  hash1to3  14401  fundmge2nop0  14411  fi1uzind  14416  brfi1indALT  14419  sswrd  14431  swrdnd2  14565  swrdnnn0nd  14566  swrdnd0  14567  swrdwrdsymb  14572  pfxnd0  14598  swrdswrdlem  14613  swrdswrd  14614  wrd2ind  14632  swrdccatin1  14634  swrdccatin2  14638  pfxccatin12lem2  14640  pfxccat3  14643  repsdf2  14687  repswswrd  14693  cshw0  14703  cshwcl  14707  cshwlen  14708  cshf1  14719  swrdco  14746  relexpsucnnl  14939  rtrclreclem3  14969  rtrclreclem4  14970  relexpindlem  14972  rtrclind  14974  shftlem  14977  caubnd  15268  reusq0  15374  rlimcld2  15487  o1dif  15539  climub  15571  climserle  15572  iseraltlem2  15592  sumss  15633  fsumzcl2  15648  fsummsnunz  15663  fsumsplitsnun  15664  fsum2d  15680  modfsummods  15702  fsumabs  15710  fsumrlim  15720  fsumo1  15721  fsumiun  15730  climcndslem1  15758  climcndslem2  15759  cvgrat  15792  clim2prod  15797  prodfn0  15803  prodfrec  15804  ntrivcvg  15806  prodmo  15845  fprodss  15857  fprodabs  15883  fprodn0  15888  fprod2d  15890  fprodefsum  16004  ruclem8  16148  ruclem9  16149  dvdsmod0  16171  dvds2ln  16202  dvdsaddre2b  16220  dvdslelem  16222  dvdsdivcl  16229  alzdvds  16233  mod2eq1n2dvds  16260  oddnn02np1  16261  nn0o1gt2  16294  nno  16295  sumeven  16300  sumodd  16301  pwp1fsum  16304  ndvdsadd  16323  bitsinv1  16355  sadcadd  16371  sadadd2  16373  saddisjlem  16377  smuval2  16395  smupvallem  16396  smu01lem  16398  smupval  16401  smueqlem  16403  smumullem  16405  gcddiv  16464  rplpwr  16471  nn0seqcvgd  16483  seq1st  16484  alginv  16488  algcvga  16492  algfx  16493  absprodnn  16531  isprm2  16595  isprm3  16596  prmind2  16598  maxprmfct  16622  prmdvdsexp  16628  pcmpt  16806  prmreclem4  16833  vdwmc2  16893  vdwlem10  16904  ramub2  16928  ramcl  16943  prmgaplem5  16969  prmgaplem8  16972  cshwshashlem1  17009  cshwshashlem3  17011  setsn0fun  17086  imasleval  17447  divsfval  17453  mreexexlem4d  17555  isssc  17729  initoeu1  17920  termoeu1  17927  istos  18324  chnfibg  18544  mgmcl  18553  sgrpidmnd  18649  frmdgsum  18772  smndex1mgm  18817  dfgrp3lem  18953  mhmmulg  19030  resghm2b  19148  gsumwrev  19280  elsymgbas  19288  symgextf1  19335  gsmsymgreqlem2  19345  gsmsymgreq  19346  odlem1  19449  odcl2  19479  gexlem1  19493  efgi2  19639  efginvrel2  19641  efgsrel  19648  cyggexb  19813  gsummulglem  19855  gsumzunsnd  19870  gsum2dlem2  19885  telgsums  19907  dmdprd  19914  dprdw  19926  ablfac1eulem  19988  srgpcomp  20138  rnghmmul  20369  nrhmzr  20454  lmodfopnelem1  20833  rmodislmodlem  20864  cnfldmulg  21342  cnfldexp  21343  nzerooringczr  21419  obslbs  21669  mplcoe1  21973  mplcoe3  21974  mplcoe5  21976  cply1mul  22212  coe1fzgsumdlem  22219  gsummoncoe1  22224  pf1ind  22271  evl1gsumdlem  22272  mat1dimcrng  22393  ma1repveval  22487  mulmarep1gsum2  22490  gsummatr01lem3  22573  cramerlem3  22605  decpmatmulsumfsupp  22689  mp2pm2mplem4  22725  pm2mpmhmlem1  22734  fvmptnn04if  22765  cayhamlem1  22782  fctop  22920  mretopd  23008  restopnb  23091  restdis  23094  tgcnp  23169  cncls2  23189  cncls  23190  cnntr  23191  cnsscnp  23195  cmpsub  23316  2ndcsep  23375  1stcelcls  23377  lfinpfin  23440  locfincmp  23442  comppfsc  23448  txcn  23542  txlm  23564  xkohaus  23569  qtopres  23614  haushmphlem  23703  cmphmph  23704  connhmph  23705  reghmph  23709  nrmhmph  23710  ptcmpfi  23729  reghaus  23741  fbssfi  23753  fbun  23756  fbfinnfr  23757  isfildlem  23773  fgcl  23794  cfinfil  23809  supfil  23811  ufinffr  23845  fin1aufil  23848  cnpflf  23917  alexsubALTlem3  23965  alexsubALT  23967  cnextfvval  23981  cnextcn  23983  tmdgsum  24011  tgphaus  24033  tgpt1  24034  mettri  24268  blssexps  24342  blssex  24343  mopni3  24410  metss  24424  psmetutop  24483  dscmet  24488  tngngp3  24572  rectbntr0  24749  metnrmlem1a  24775  fsumcn  24789  lmmbr  25186  caubl  25236  caublcls  25237  bcthlem5  25256  bcth3  25259  ovolunlem1a  25425  ovoliunnul  25436  finiunmbl  25473  voliunlem1  25479  volsuplem  25484  volsup  25485  dyadmax  25527  itgfsum  25756  dvnadd  25859  cpnord  25865  dvnfre  25884  dvmptfsum  25907  dvlip  25926  fta1g  26103  plyco  26174  dgrcolem1  26207  dgrco  26209  dvnply2  26223  plydivex  26233  plyexmo  26249  aannenlem1  26264  aaliou3lem2  26279  dvntaylp  26307  taylthlem1  26309  ulmval  26317  cxpmul2  26626  cxpsqrtth  26667  scvxcvx  26924  jensenlem2  26926  jensen  26927  ppiub  27143  bcmono  27216  bpos1lem  27221  bposlem5  27227  gausslemma2dlem6  27311  lgsquad2lem2  27324  2lgslem3  27343  2lgs  27346  2sqnn  27378  addsqnreup  27382  2sqreultblem  27387  2sqreunnltblem  27390  dchrisumlem1  27428  dchrisum0flb  27449  pntpbnd1  27525  pntlemf  27544  qabvle  27564  qabvexp  27565  ostthlem2  27567  ostth2lem2  27573  sltval2  27596  sltsolem1  27615  negsprop  27978  mulsuniflem  28089  precsexlem6  28151  precsexlem7  28152  noseqind  28223  om2noseqlt  28230  n0addscl  28273  n0mulscl  28274  expsne0  28360  axeuclidlem  28942  axcontlem12  28955  umgrnloopv  29086  uhgredgrnv  29110  edglnl  29123  numedglnl  29124  usgruspgrb  29163  usgrnloopvALT  29181  usgredg2vlem2  29206  subupgr  29267  nbumgr  29327  uhgrnbgr0nb  29334  nbgr0edglem  29336  edgusgrnbfin  29353  nb3grprlem2  29361  uvtxnbgrvtx  29373  cplgrop  29417  cusgrfi  29439  fusgrmaxsize  29445  fusgrn0degnn0  29480  ewlkprop  29584  uspgr2wlkeq  29626  g0wlk0  29631  wlkreslem  29648  lfgriswlk  29667  upgrwlkdvde  29717  spthonepeq  29732  uhgrwkspth  29735  usgr2trlncl  29740  usgr2trlspth  29741  cyclnumvtx  29780  cyclnspth  29781  crctcshwlkn0lem3  29792  wwlksn  29817  wspthneq1eq2  29840  wwlksm1edg  29861  wwlksnred  29872  wwlksnextfun  29878  wwlksnextinj  29879  wwlksnextproplem3  29891  wspthsnonn0vne  29897  wspn0  29904  rusgrnumwwlk  29958  clwwlkccatlem  29971  umgrclwwlkge2  29973  clwlkclwwlklem2  29982  clwlkclwwlklem3  29983  clwwisshclwws  29997  clwwisshclwwsn  29998  clwwlkn1loopb  30025  wwlksext2clwwlk  30039  wwlksubclwwlk  30040  clwwlknonex2lem2  30090  upgr3v3e3cycl  30162  uhgr3cyclex  30164  upgr4cycl4dv4e  30167  eupth2lem3lem4  30213  eupth2lem3lem7  30216  eupth2  30221  eulerpath  30223  nfrgr2v  30254  frgr3vlem1  30255  3vfriswmgr  30260  1to2vfriswmgr  30261  1to3vfriswmgr  30262  3cyclfrgrrn1  30267  3cyclfrgrrn  30268  3cyclfrgrrn2  30269  4cycl2vnunb  30272  frgrncvvdeqlem2  30282  frgrncvvdeqlem8  30288  frgrncvvdeqlem9  30289  frgrwopreglem4a  30292  frgrwopreglem5lem  30302  frgrwopreglem5ALT  30304  frgrregorufr0  30306  frgr2wwlk1  30311  frgr2wwlkeqm  30313  fusgr2wsp2nb  30316  2wspmdisj  30319  frrusgrord  30323  numclwwlk1lem2f1  30339  numclwlk1  30353  frgrreggt1  30375  friendshipgt3  30380  hlim2  31174  elnlfn  31910  stle0i  32221  hstrbi  32248  spansncv2  32275  h1da  32331  fmptcof2  32641  sgn3da  32822  xreceu  32909  domnprodn0  33249  1arithufdlem3  33518  1arithufdlem4  33519  tpr2rico  33946  hasheuni  34119  ismeas  34233  sseqp1  34429  rrvsum  34488  dstfrvunirn  34509  signstfvc  34608  bnj607  34949  bnj1145  35026  bnj1204  35045  r1filim  35136  fineqvrep  35158  fineqvnttrclselem1  35162  onvf1odlem4  35171  fisshasheq  35180  subgrwlk  35197  subfacp1lem6  35250  cvmlift2lem12  35379  cvmlift3lem4  35387  satfrnmapom  35435  sat1el2xp  35444  satffunlem2  35473  satffun  35474  mrsubvrs  35587  climuzcnv  35736  iprodefisumlem  35805  dfon2lem9  35854  linethru  36218  elhf2  36240  finminlem  36383  fnessref  36422  neibastop2lem  36425  fnemeet2  36432  nndivsub  36522  bj-xpnzex  37024  bj-elpwg  37117  bj-epelg  37133  mptsnunlem  37403  dissneqlem  37405  topdifinffinlem  37412  iooelexlt  37427  domalom  37469  fvineqsneq  37477  wl-exeq  37599  matunitlindflem1  37676  poimirlem22  37702  poimirlem26  37706  poimirlem28  37708  poimirlem29  37709  poimirlem32  37712  heicant  37715  ovoliunnfl  37722  voliunnfl  37724  volsupnfl  37725  cover2  37775  upixp  37789  sdclem2  37802  fdc  37805  seqpo  37807  metf1o  37815  mettrifi  37817  sstotbnd3  37836  heibor1lem  37869  heiborlem5  37875  heibor  37881  bfplem1  37882  elghomlem2OLD  37946  grpokerinj  37953  isrngo  37957  rngodm1dm2  37992  ispridl2  38098  exlimddvf  38181  lssatle  39134  4atexlemex4  40192  uzindd  42090  evl1gprodd  42230  sn-axprlem3  42335  redvmptabs  42478  sn-sup3d  42610  mzpsubst  42865  jm2.18  43105  wepwsolem  43159  oaabsb  43411  oacl2g  43447  ofoafg  43471  ofoaid1  43475  ofoaid2  43476  naddonnn  43512  iunrelexp0  43819  relexpmulg  43827  cnvtrclfv  43841  clsk1indlem3  44160  grucollcld  44377  inaex  44414  dvgrat  44429  radcnvrat  44431  csbxpgVD  45010  sineq0ALT  45053  trfr  45079  relwf  45084  pwclaxpow  45101  omssaxinf2  45105  islptre  45743  iblspltprt  46095  stoweidlem2  46124  stoweidlem17  46139  stoweidlem21  46143  2reuimp0  47238  2reuimp  47239  afveu  47277  funbrafv  47282  ndmaovass  47330  afv2eu  47362  tz6.12c-afv2  47366  funop1  47407  f1oresf1o2  47415  fvmptrabdm  47417  nltle2tri  47437  2elfz2melfz  47442  fsummsndifre  47496  fsumsplitsndif  47497  fsummmodsndifre  47498  fsummmodsnunz  47499  elsetpreimafvssdm  47510  uniimaelsetpreimafv  47520  imasetpreimafvbijlemfv1  47527  iccpartiltu  47546  iccpartigtl  47547  iccpartleu  47552  iccpartgel  47553  iccpartrn  47554  iccpartiun  47558  icceuelpart  47560  iccpartnel  47562  fargshiftf  47564  fargshiftf1  47565  ichnfb  47589  elsprel  47599  prsprel  47611  sprsymrelfo  47621  paireqne  47635  sbcpr  47645  reupr  47646  fmtnoinf  47660  odz2prm2pw  47687  lighneallem4  47734  lighneal  47735  requad1  47746  requad2  47747  evensumeven  47831  even3prm2  47843  gbowgt5  47886  nnsum4primeseven  47924  nnsum4primesevenALTV  47925  bgoldbnnsum3prm  47928  bgoldbtbndlem2  47930  bgoldbtbndlem4  47932  bgoldbtbnd  47933  dfsclnbgr6  47982  grimco  48013  cycl3grtri  48071  isubgr3stgrlem6  48095  gricgrlic  48142  gpgedgvtx0  48185  gpgprismgr4cycllem3  48221  pgnbgreunbgrlem5  48247  clcllaw  48315  rngccatidALTV  48396  ringccatidALTV  48430  scmsuppss  48495  gsumlsscl  48504  ply1mulgsumlem2  48512  lincvalsc0  48546  linc0scn0  48548  lincdifsn  48549  linc1  48550  lincellss  48551  lincsum  48554  lincscm  48555  lincsumcl  48556  lcoss  48561  lincext3  48581  lindslinindimp2lem4  48586  lindslinindsimp2lem5  48587  lindslinindsimp2  48588  lindsrng01  48593  snlindsntor  48596  lincresunit3lem2  48605  lincresunit3  48606  islindeps2  48608  blengt1fldiv2p1  48718  2arymaptf1  48778  resum2sqorgt0  48834  reorelicc  48835  rrx2plordisom  48848  rrx2linest  48867  rrxsphere  48873  line2ylem  48876  itsclc0xyqsol  48893  itscnhlinecirc02p  48910  mo0sn  48940  thincn0eu  49556