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

This theorem is referenced by:  ancoms  458  pm3.21  471  sylan  579  animpimp2impd  842  4casesdan  1038  dedlema  1042  dedlemb  1043  sbiedvw  2098  cbval2vOLD  2343  mo4  2566  2moswapv  2631  2moswap  2646  2mos  2651  2eu2  2654  pm2.61ne  3029  nelelne  3042  r19.21be  3133  cbvraldva2  3381  rspcebdv  3545  2reu2  3827  csbie2df  4371  minel  4396  uneqdifeq  4420  raltpd  4714  ssunsn2  4757  opthprneg  4792  ssuni  4863  uniss2  4871  elpwuni  5030  intss2  5033  disjord  5058  elssabg  5255  elpw2g  5263  axprlem3  5343  axprlem4  5344  axprlem5  5345  oteqex  5408  otsndisj  5427  otiunsndisj  5428  epelg  5487  wereu  5576  relop  5748  riinint  5866  sotri3  6024  unixpid  6176  reuop  6185  ordtr2  6295  ordsssuc2  6339  iotan0  6408  funopg  6452  fun  6620  tz6.12c  6781  fvmptnf  6879  fvn0ssdmfun  6934  eldmrexrnb  6950  fmptco  6983  fnressn  7012  fressnfv  7014  fprb  7051  fvtp2g  7056  fvtp3g  7057  fconst2g  7060  fntpb  7067  f1dom3el3dif  7123  isores3  7186  isoselem  7192  oprabv  7313  eloprabga  7360  eloprabgaOLD  7361  sorpsscmpl  7565  difex2  7588  ordpwsuc  7637  ordsucun  7647  limuni3  7674  trom  7696  fo1stres  7830  poxp  7940  soxp  7941  suppimacnv  7961  frnsuppeq  7962  funsssuppss  7977  brtpos2  8019  frrlem8  8080  fpr2a  8089  wfrlem12OLD  8122  onnseq  8146  smores  8154  smofvon2  8158  tfrlem1  8178  oacl  8327  omcl  8328  oecl  8329  oawordri  8343  oalimcl  8353  oaass  8354  oarec  8355  omwordri  8365  omeulem1  8375  omeulem2  8376  oeordi  8380  oeworde  8386  oeoelem  8391  nnacl  8404  nnmcl  8405  nnecl  8406  nnacom  8410  nnaass  8415  nnmsucr  8418  nnmordi  8424  omabs  8441  iiner  8536  elpmg  8589  fsetfcdm  8606  fsetprcnex  8608  pmss12g  8615  mapfvd  8625  f1domg  8715  ssdomg  8741  domtriord  8859  php  8897  php3  8899  ssnnfi  8914  ssnnfiOLD  8915  imafi  8920  fnfi  8925  enfi  8933  1sdom  8955  fisseneq  8963  isinf  8965  dif1enALT  8980  findcard3  8987  frfi  8989  unfiOLD  9011  difinf  9014  iunfi  9037  fsuppunfi  9078  fsuppres  9083  frnfsuppbi  9087  elfi2  9103  marypha1lem  9122  marypha1  9123  oiexg  9224  wemapso2  9242  harword  9252  brwdom  9256  unxpwdom  9278  en3lplem1  9300  inf3lemd  9315  inf3lem5  9320  cantnfval2  9357  cantnfle  9359  cantnflt  9360  cnfcom  9388  trpredtr  9408  trpredmintr  9409  dftrpred3g  9412  trpredrec  9415  tcmin  9430  frr2  9449  r1sdom  9463  rankxplim3  9570  cardidm  9648  cardmin2  9688  infxpenlem  9700  fseqenlem1  9711  numacn  9736  alephordi  9761  iscard3  9780  alephinit  9782  carduniima  9783  iunfictbso  9801  dfac5  9815  dfac12lem3  9832  nnadju  9884  pwsdompw  9891  pwdjudom  9903  cflim2  9950  cfslb2n  9955  cofsmo  9956  cfsmolem  9957  cfcoflem  9959  alephsing  9963  infpssALT  10000  fin23lem34  10033  isf32lem2  10041  isf32lem10  10049  isf32lem12  10051  isfin1-2  10072  hsmexlem4  10116  axcc2lem  10123  domtriomlem  10129  axdc2lem  10135  axdc3lem2  10138  axdc3lem4  10140  axdc4lem  10142  axcclem  10144  ac6num  10166  ac6s  10171  zorn2lem7  10189  ttukeylem5  10200  imadomg  10221  iundom2g  10227  ondomon  10250  ficard  10252  konigthlem  10255  alephreg  10269  pwcfsdom  10270  cfpwsdom  10271  axregndlem1  10289  axregnd  10291  pwfseqlem3  10347  pwxpndom2  10352  pwxpndom  10353  pwdjundom  10354  inawinalem  10376  gchina  10386  wuncval2  10434  tsk0  10450  tskxpss  10459  inatsk  10465  tskuni  10470  gruina  10505  grothac  10517  addclpi  10579  addnidpi  10588  nqereu  10616  mulcanenq  10647  genpnnp  10692  nqpr  10701  prlem934  10720  reclem2pr  10735  suplem1pr  10739  supsrlem  10798  axpre-sup  10856  1re  10906  dedekindle  11069  00id  11080  receu  11550  sup3  11862  infrelb  11890  peano5nni  11906  nnindd  11923  nnaddcl  11926  zrevaddcl  12295  nzadd  12298  zdiv  12320  nneo  12334  zeo2  12337  nn0indd  12347  fzind  12348  fnn0ind  12349  uzwo  12580  lbzbi  12605  nn01to3  12610  qrevaddcl  12640  irradd  12642  irrmul  12643  ltsubrp  12695  ltaddrp  12696  xnn0xaddcl  12898  xnn0xadd0  12910  icoshft  13134  fzen  13202  elfzm11  13256  uzsplit  13257  elfzoext  13372  elfzom1elp1fzo  13382  injresinjlem  13435  injresinj  13436  modifeq2int  13581  modsumfzodifsn  13592  om2uzlti  13598  ssnn0fi  13633  fsuppmapnn0fiub0  13641  mptnn0fsuppr  13647  seqcaopr3  13686  seqf1olem2a  13689  seqf1o  13692  ser1const  13707  expadd  13753  expmul  13756  leexp1a  13821  faccl  13925  facdiv  13929  faclbnd  13932  faclbnd4lem4  13938  hasheqf1oi  13994  hashgadd  14020  hashinfxadd  14028  hashunx  14029  hashunsng  14035  elprchashprn2  14039  hashss  14052  hash1snb  14062  hashmap  14078  hashf1lem2  14098  hashf1  14099  seqcoll  14106  hashle2pr  14119  hashdmpropge2  14125  hashge3el3dif  14128  hash1to3  14133  fundmge2nop0  14134  fi1uzind  14139  brfi1indALT  14142  sswrd  14153  swrdnd2  14296  swrdnnn0nd  14297  swrdnd0  14298  swrdwrdsymb  14303  pfxnd0  14329  swrdswrdlem  14345  swrdswrd  14346  wrd2ind  14364  swrdccatin1  14366  swrdccatin2  14370  pfxccatin12lem2  14372  pfxccat3  14375  repsdf2  14419  repswswrd  14425  cshw0  14435  cshwcl  14439  cshwlen  14440  cshf1  14451  swrdco  14478  relexpsucnnl  14669  rtrclreclem3  14699  rtrclreclem4  14700  relexpindlem  14702  rtrclind  14704  shftlem  14707  caubnd  14998  reusq0  15102  rlimcld2  15215  o1dif  15267  climub  15301  climserle  15302  iseraltlem2  15322  sumss  15364  fsumzcl2  15379  fsummsnunz  15394  fsumsplitsnun  15395  fsum2d  15411  modfsummods  15433  fsumabs  15441  fsumrlim  15451  fsumo1  15452  fsumiun  15461  climcndslem1  15489  climcndslem2  15490  cvgrat  15523  clim2prod  15528  prodfn0  15534  prodfrec  15535  ntrivcvg  15537  prodmo  15574  fprodss  15586  fprodabs  15612  fprodn0  15617  fprod2d  15619  fprodefsum  15732  ruclem8  15874  ruclem9  15875  dvdsmod0  15897  dvds2ln  15926  dvdsaddre2b  15944  dvdslelem  15946  dvdsdivcl  15953  alzdvds  15957  mod2eq1n2dvds  15984  oddnn02np1  15985  nn0o1gt2  16018  nno  16019  sumeven  16024  sumodd  16025  pwp1fsum  16028  ndvdsadd  16047  bitsinv1  16077  sadcadd  16093  sadadd2  16095  saddisjlem  16099  smuval2  16117  smupvallem  16118  smu01lem  16120  smupval  16123  smueqlem  16125  smumullem  16127  gcddiv  16187  gcdmultipleOLD  16188  rplpwr  16195  nn0seqcvgd  16203  seq1st  16204  alginv  16208  algcvga  16212  algfx  16213  absprodnn  16251  isprm2  16315  isprm3  16316  prmind2  16318  maxprmfct  16342  prmdvdsexp  16348  pcmpt  16521  prmreclem4  16548  vdwmc2  16608  vdwlem10  16619  ramub2  16643  ramcl  16658  prmgaplem5  16684  prmgaplem8  16687  cshwshashlem1  16725  cshwshashlem3  16727  setsn0fun  16802  imasleval  17169  divsfval  17175  mreexexlem4d  17273  isssc  17449  initoeu1  17642  termoeu1  17649  istos  18051  mgmcl  18244  sgrpidmnd  18305  frmdgsum  18416  smndex1mgm  18461  dfgrp3lem  18588  mhmmulg  18659  resghm2b  18767  gsumwrev  18888  elsymgbas  18896  symgextf1  18944  gsmsymgreqlem2  18954  gsmsymgreq  18955  odlem1  19058  odcl2  19087  gexlem1  19099  efgi2  19246  efginvrel2  19248  efgsrel  19255  cyggexb  19415  gsummulglem  19457  gsumzunsnd  19472  gsum2dlem2  19487  telgsums  19509  dmdprd  19516  dprdw  19528  ablfac1eulem  19590  srgpcomp  19683  lmodfopnelem1  20074  rmodislmodlem  20105  cnfldmulg  20542  cnfldexp  20543  obslbs  20847  mplcoe1  21148  mplcoe3  21149  mplcoe5  21151  cply1mul  21375  coe1fzgsumdlem  21382  gsummoncoe1  21385  pf1ind  21431  evl1gsumdlem  21432  mat1dimcrng  21534  ma1repveval  21628  mulmarep1gsum2  21631  gsummatr01lem3  21714  cramerlem3  21746  decpmatmulsumfsupp  21830  mp2pm2mplem4  21866  pm2mpmhmlem1  21875  fvmptnn04if  21906  cayhamlem1  21923  fctop  22062  mretopd  22151  restopnb  22234  restdis  22237  tgcnp  22312  cncls2  22332  cncls  22333  cnntr  22334  cnsscnp  22338  cmpsub  22459  2ndcsep  22518  1stcelcls  22520  lfinpfin  22583  locfincmp  22585  comppfsc  22591  txcn  22685  txlm  22707  xkohaus  22712  qtopres  22757  haushmphlem  22846  cmphmph  22847  connhmph  22848  reghmph  22852  nrmhmph  22853  ptcmpfi  22872  reghaus  22884  fbssfi  22896  fbun  22899  fbfinnfr  22900  isfildlem  22916  fgcl  22937  cfinfil  22952  supfil  22954  ufinffr  22988  fin1aufil  22991  cnpflf  23060  alexsubALTlem3  23108  alexsubALT  23110  cnextfvval  23124  cnextcn  23126  tmdgsum  23154  tgphaus  23176  tgpt1  23177  mettri  23413  blssexps  23487  blssex  23488  mopni3  23556  metss  23570  psmetutop  23629  dscmet  23634  tngngp3  23726  rectbntr0  23901  metnrmlem1a  23927  fsumcn  23939  lmmbr  24327  caubl  24377  caublcls  24378  bcthlem5  24397  bcth3  24400  ovolunlem1a  24565  ovoliunnul  24576  finiunmbl  24613  voliunlem1  24619  volsuplem  24624  volsup  24625  dyadmax  24667  itgfsum  24896  dvnadd  24998  cpnord  25004  dvnfre  25021  dvmptfsum  25044  dvlip  25062  fta1g  25237  plyco  25307  dgrcolem1  25339  dgrco  25341  dvnply2  25352  plydivex  25362  plyexmo  25378  aannenlem1  25393  aaliou3lem2  25408  dvntaylp  25435  taylthlem1  25437  ulmval  25444  cxpmul2  25749  cxpsqrtth  25789  scvxcvx  26040  jensenlem2  26042  jensen  26043  ppiub  26257  bcmono  26330  bpos1lem  26335  bposlem5  26341  gausslemma2dlem6  26425  lgsquad2lem2  26438  2lgslem3  26457  2lgs  26460  2sqnn  26492  addsqnreup  26496  2sqreultblem  26501  2sqreunnltblem  26504  dchrisumlem1  26542  dchrisum0flb  26563  pntpbnd1  26639  pntlemf  26658  qabvle  26678  qabvexp  26679  ostthlem2  26681  ostth2lem2  26687  axeuclidlem  27233  axcontlem12  27246  umgrnloopv  27379  uhgredgrnv  27403  edglnl  27416  numedglnl  27417  usgruspgrb  27454  usgrnloopvALT  27471  usgredg2vlem2  27496  subupgr  27557  nbumgr  27617  uhgrnbgr0nb  27624  nbgr0vtxlem  27625  edgusgrnbfin  27643  nb3grprlem2  27651  uvtxnbgrvtx  27663  cplgrop  27707  cusgrfi  27728  fusgrmaxsize  27734  fusgrn0degnn0  27769  ewlkprop  27873  uspgr2wlkeq  27915  g0wlk0  27921  wlkreslem  27939  lfgriswlk  27958  upgrwlkdvde  28006  spthonepeq  28021  uhgrwkspth  28024  usgr2trlncl  28029  usgr2trlspth  28030  cyclnspth  28069  crctcshwlkn0lem3  28078  wwlksn  28103  wspthneq1eq2  28126  wwlksm1edg  28147  wwlksnred  28158  wwlksnextfun  28164  wwlksnextinj  28165  wwlksnextproplem3  28177  wspthsnonn0vne  28183  wspn0  28190  rusgrnumwwlk  28241  clwwlkccatlem  28254  umgrclwwlkge2  28256  clwlkclwwlklem2  28265  clwlkclwwlklem3  28266  clwwisshclwws  28280  clwwisshclwwsn  28281  clwwlkn1loopb  28308  wwlksext2clwwlk  28322  wwlksubclwwlk  28323  clwwlknonex2lem2  28373  upgr3v3e3cycl  28445  uhgr3cyclex  28447  upgr4cycl4dv4e  28450  eupth2lem3lem4  28496  eupth2lem3lem7  28499  eupth2  28504  eulerpath  28506  nfrgr2v  28537  frgr3vlem1  28538  3vfriswmgr  28543  1to2vfriswmgr  28544  1to3vfriswmgr  28545  3cyclfrgrrn1  28550  3cyclfrgrrn  28551  3cyclfrgrrn2  28552  4cycl2vnunb  28555  frgrncvvdeqlem2  28565  frgrncvvdeqlem8  28571  frgrncvvdeqlem9  28572  frgrwopreglem4a  28575  frgrwopreglem5lem  28585  frgrwopreglem5ALT  28587  frgrregorufr0  28589  frgr2wwlk1  28594  frgr2wwlkeqm  28596  fusgr2wsp2nb  28599  2wspmdisj  28602  frrusgrord  28606  numclwwlk1lem2f1  28622  numclwlk1  28636  frgrreggt1  28658  friendshipgt3  28663  hlim2  29455  elnlfn  30191  stle0i  30502  hstrbi  30529  spansncv2  30556  h1da  30612  fmptcof2  30896  xreceu  31098  tpr2rico  31764  hasheuni  31953  ismeas  32067  sseqp1  32262  rrvsum  32321  dstfrvunirn  32341  sgn3da  32408  signstfvc  32453  bnj607  32796  bnj1145  32873  bnj1204  32892  fineqvrep  32964  fisshasheq  32973  subgrwlk  32994  subfacp1lem6  33047  cvmlift2lem12  33176  cvmlift3lem4  33184  satfrnmapom  33232  sat1el2xp  33241  satffunlem2  33270  satffun  33271  mrsubvrs  33384  climuzcnv  33529  iprodefisumlem  33612  dfon2lem9  33673  soseq  33730  sltval2  33786  sltsolem1  33805  linethru  34382  elhf2  34404  finminlem  34434  fnessref  34473  neibastop2lem  34476  fnemeet2  34483  nndivsub  34573  bj-xpnzex  35076  bj-elpwg  35152  bj-epelg  35166  mptsnunlem  35436  dissneqlem  35438  topdifinffinlem  35445  iooelexlt  35460  domalom  35502  fvineqsneq  35510  wl-exeq  35620  wl-ax11-lem3  35665  matunitlindflem1  35700  poimirlem22  35726  poimirlem26  35730  poimirlem28  35732  poimirlem29  35733  poimirlem32  35736  heicant  35739  ovoliunnfl  35746  voliunnfl  35748  volsupnfl  35749  cover2  35799  upixp  35814  sdclem2  35827  fdc  35830  seqpo  35832  metf1o  35840  mettrifi  35842  sstotbnd3  35861  heibor1lem  35894  heiborlem5  35900  heibor  35906  bfplem1  35907  elghomlem2OLD  35971  grpokerinj  35978  isrngo  35982  rngodm1dm2  36017  ispridl2  36123  exlimddvf  36206  lssatle  36956  4atexlemex4  38014  fzindd  39912  uzindd  39913  sn-axprlem3  40114  mzpsubst  40486  jm2.18  40726  wepwsolem  40783  iunrelexp0  41199  relexpmulg  41207  cnvtrclfv  41221  clsk1indlem3  41542  grucollcld  41767  inaex  41804  dvgrat  41819  radcnvrat  41821  csbxpgVD  42403  sineq0ALT  42446  islptre  43050  iblspltprt  43404  stoweidlem2  43433  stoweidlem17  43448  stoweidlem21  43452  2reuimp0  44493  2reuimp  44494  afveu  44532  funbrafv  44537  ndmaovass  44585  afv2eu  44617  tz6.12c-afv2  44621  funop1  44662  f1oresf1o2  44670  fvmptrabdm  44672  nltle2tri  44693  2elfz2melfz  44698  fzoopth  44707  fsummsndifre  44712  fsumsplitsndif  44713  fsummmodsndifre  44714  fsummmodsnunz  44715  elsetpreimafvssdm  44726  uniimaelsetpreimafv  44736  imasetpreimafvbijlemfv1  44743  iccpartiltu  44762  iccpartigtl  44763  iccpartleu  44768  iccpartgel  44769  iccpartrn  44770  iccpartiun  44774  icceuelpart  44776  iccpartnel  44778  fargshiftf  44780  fargshiftf1  44781  ichnfb  44805  elsprel  44815  prsprel  44827  sprsymrelfo  44837  paireqne  44851  sbcpr  44861  reupr  44862  fmtnoinf  44876  odz2prm2pw  44903  lighneallem4  44950  lighneal  44951  requad1  44962  requad2  44963  evensumeven  45047  even3prm2  45059  gbowgt5  45102  nnsum4primeseven  45140  nnsum4primesevenALTV  45141  bgoldbnnsum3prm  45144  bgoldbtbndlem2  45146  bgoldbtbndlem4  45148  bgoldbtbnd  45149  isomuspgrlem1  45167  clcllaw  45273  nrhmzr  45319  rnghmmul  45346  rngccatidALTV  45435  ringccatidALTV  45498  nzerooringczr  45518  scmsuppss  45596  gsumlsscl  45607  ply1mulgsumlem2  45616  lincvalsc0  45650  linc0scn0  45652  lincdifsn  45653  linc1  45654  lincellss  45655  lincsum  45658  lincscm  45659  lincsumcl  45660  lcoss  45665  lincext3  45685  lindslinindimp2lem4  45690  lindslinindsimp2lem5  45691  lindslinindsimp2  45692  lindsrng01  45697  snlindsntor  45700  lincresunit3lem2  45709  lincresunit3  45710  islindeps2  45712  blengt1fldiv2p1  45827  2arymaptf1  45887  resum2sqorgt0  45943  reorelicc  45944  rrx2plordisom  45957  rrx2linest  45976  rrxsphere  45982  line2ylem  45985  itsclc0xyqsol  46002  itscnhlinecirc02p  46019  mo0sn  46049  thincn0eu  46201