Theorem expcom 412

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

Syntax hints:   → wi 4   ∧ wa 394

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 395

This theorem is referenced by:  ancoms  457  pm3.21  470  sylan  578  animpimp2impd  844  4casesdan  1039  dedlema  1043  dedlemb  1044  sbiedvw  2088  mo4  2554  2moswapv  2617  2moswap  2632  2mosOLD  2638  2eu2  2641  pm2.61ne  3016  nelelne  3030  r19.21be  3239  cbvraldva2  3331  rspcebdv  3600  2reu2  3888  csbie2df  4442  minel  4467  uneqdifeq  4494  raltpd  4787  ssunsn2  4832  opthprneg  4867  ssuni  4936  uniss2  4945  elpwuni  5109  intss2  5112  disjord  5137  elssabg  5339  elpw2g  5347  axprlem3  5425  axprlem4  5426  axprlem5  5427  oteqex  5502  otsndisj  5521  otiunsndisj  5522  epelg  5583  wereu  5674  relop  5853  riinint  5971  sotri3  6137  unixpid  6290  reuop  6299  ordtr2  6415  ordsssuc2  6462  iotan0  6539  funopg  6588  fun  6759  tz6.12cOLD  6923  fvmptnf  7026  fvn0ssdmfun  7083  eldmrexrnb  7101  fmptco  7138  fnressn  7167  fressnfv  7169  fprb  7206  fvtp2g  7211  fvtp3g  7212  fconst2g  7215  fntpb  7221  f1dom3el3dif  7279  isores3  7342  isoselem  7348  oprabv  7480  eloprabga  7528  eloprabgaOLD  7529  sorpsscmpl  7740  difex2  7763  ordpwsuc  7819  ordsucun  7829  limuni3  7857  trom  7880  fo1stres  8020  poxp  8133  soxp  8134  xpord3inddlem  8159  soseq  8164  suppimacnv  8179  fsuppeq  8180  funsssuppss  8195  brtpos2  8238  frrlem8  8299  fpr2a  8308  wfrlem12OLD  8341  onnseq  8365  smores  8373  smofvon2  8377  tfrlem1  8397  oacl  8556  omcl  8557  oecl  8558  oawordri  8571  oalimcl  8581  oaass  8582  oarec  8583  omwordri  8593  omeulem1  8603  omeulem2  8604  oeordi  8608  oeworde  8614  oeoelem  8619  nnacl  8632  nnmcl  8633  nnecl  8634  nnacom  8638  nnaass  8643  nnmsucr  8646  nnmordi  8652  omabs  8672  cofonr  8695  naddunif  8714  iiner  8808  elpmg  8862  fsetfcdm  8879  fsetprcnex  8881  pmss12g  8888  mapfvd  8898  f1domg  8993  ssdomg  9021  undom  9087  domtriord  9151  ssnnfi  9197  ssnnfiOLD  9198  imafi  9203  fnfi  9209  enfi  9218  php  9238  phpOLD  9250  php3OLD  9252  sdom1  9270  1sdom2dom  9275  1sdomOLD  9277  fisseneq  9285  isinf  9288  isinfOLD  9289  dif1ennnALT  9305  findcard3  9313  findcard3OLD  9314  frfi  9316  unfiOLD  9341  difinf  9345  iunfi  9371  fsuppunfi  9418  fsuppres  9423  ffsuppbi  9428  elfi2  9444  marypha1lem  9463  marypha1  9464  oiexg  9565  wemapso2  9583  harword  9593  brwdom  9597  unxpwdom  9619  en3lplem1  9642  inf3lemd  9657  inf3lem5  9662  cantnfval2  9699  cantnfle  9701  cantnflt  9702  cnfcom  9730  tcmin  9771  frr2  9790  r1sdom  9804  rankxplim3  9911  cardidm  9989  cardmin2  10029  infxpenlem  10043  fseqenlem1  10054  numacn  10079  alephordi  10104  iscard3  10123  alephinit  10125  carduniima  10126  iunfictbso  10144  dfac5  10158  dfac12lem3  10175  nnadju  10227  pwsdompw  10234  pwdjudom  10246  cflim2  10293  cfslb2n  10298  cofsmo  10299  cfsmolem  10300  cfcoflem  10302  alephsing  10306  infpssALT  10343  fin23lem34  10376  isf32lem2  10384  isf32lem10  10392  isf32lem12  10394  isfin1-2  10415  hsmexlem4  10459  axcc2lem  10466  domtriomlem  10472  axdc2lem  10478  axdc3lem2  10481  axdc3lem4  10483  axdc4lem  10485  axcclem  10487  ac6num  10509  ac6s  10514  zorn2lem7  10532  ttukeylem5  10543  imadomg  10564  iundom2g  10570  ondomon  10593  ficard  10595  konigthlem  10598  alephreg  10612  pwcfsdom  10613  cfpwsdom  10614  axregndlem1  10632  axregnd  10634  pwfseqlem3  10690  pwxpndom2  10695  pwxpndom  10696  pwdjundom  10697  inawinalem  10719  gchina  10729  wuncval2  10777  tsk0  10793  tskxpss  10802  inatsk  10808  tskuni  10813  gruina  10848  grothac  10860  addclpi  10922  addnidpi  10931  nqereu  10959  mulcanenq  10990  genpnnp  11035  nqpr  11044  prlem934  11063  reclem2pr  11078  suplem1pr  11082  supsrlem  11141  axpre-sup  11199  1re  11251  dedekindle  11415  00id  11426  receu  11896  sup3  12209  infrelb  12237  peano5nni  12253  nnindd  12270  nnaddcl  12273  zrevaddcl  12645  nzadd  12648  zdiv  12670  nneo  12684  zeo2  12687  nn0indd  12697  fzind  12698  fnn0ind  12699  fzindd  12702  uzwo  12933  lbzbi  12958  nn01to3  12963  qrevaddcl  12993  irradd  12995  irrmul  12996  ltsubrp  13050  ltaddrp  13051  xnn0xaddcl  13254  xnn0xadd0  13266  icoshft  13490  fzen  13558  elfzm11  13612  uzsplit  13613  elfzoext  13729  elfzom1elp1fzo  13739  fzoopth  13768  injresinjlem  13793  injresinj  13794  modifeq2int  13939  modsumfzodifsn  13950  om2uzlti  13956  ssnn0fi  13991  fsuppmapnn0fiub0  13999  mptnn0fsuppr  14005  seqcaopr3  14043  seqf1olem2a  14046  seqf1o  14049  ser1const  14064  expadd  14110  expmul  14113  leexp1a  14180  faccl  14286  facdiv  14290  faclbnd  14293  faclbnd4lem4  14299  hasheqf1oi  14354  hashgadd  14380  hashinfxadd  14388  hashunx  14389  hashunsng  14395  elprchashprn2  14399  hashss  14412  hash1snb  14422  hashmap  14438  hashf1lem2  14461  hashf1  14462  seqcoll  14469  hashle2pr  14482  hashdmpropge2  14488  hashge3el3dif  14491  hash1to3  14496  fundmge2nop0  14497  fi1uzind  14502  brfi1indALT  14505  sswrd  14516  swrdnd2  14649  swrdnnn0nd  14650  swrdnd0  14651  swrdwrdsymb  14656  pfxnd0  14682  swrdswrdlem  14698  swrdswrd  14699  wrd2ind  14717  swrdccatin1  14719  swrdccatin2  14723  pfxccatin12lem2  14725  pfxccat3  14728  repsdf2  14772  repswswrd  14778  cshw0  14788  cshwcl  14792  cshwlen  14793  cshf1  14804  swrdco  14832  relexpsucnnl  15021  rtrclreclem3  15051  rtrclreclem4  15052  relexpindlem  15054  rtrclind  15056  shftlem  15059  caubnd  15349  reusq0  15453  rlimcld2  15566  o1dif  15618  climub  15652  climserle  15653  iseraltlem2  15673  sumss  15714  fsumzcl2  15729  fsummsnunz  15744  fsumsplitsnun  15745  fsum2d  15761  modfsummods  15783  fsumabs  15791  fsumrlim  15801  fsumo1  15802  fsumiun  15811  climcndslem1  15839  climcndslem2  15840  cvgrat  15873  clim2prod  15878  prodfn0  15884  prodfrec  15885  ntrivcvg  15887  prodmo  15924  fprodss  15936  fprodabs  15962  fprodn0  15967  fprod2d  15969  fprodefsum  16083  ruclem8  16225  ruclem9  16226  dvdsmod0  16248  dvds2ln  16277  dvdsaddre2b  16295  dvdslelem  16297  dvdsdivcl  16304  alzdvds  16308  mod2eq1n2dvds  16335  oddnn02np1  16336  nn0o1gt2  16369  nno  16370  sumeven  16375  sumodd  16376  pwp1fsum  16379  ndvdsadd  16398  bitsinv1  16428  sadcadd  16444  sadadd2  16446  saddisjlem  16450  smuval2  16468  smupvallem  16469  smu01lem  16471  smupval  16474  smueqlem  16476  smumullem  16478  gcddiv  16538  rplpwr  16545  nn0seqcvgd  16557  seq1st  16558  alginv  16562  algcvga  16566  algfx  16567  absprodnn  16605  isprm2  16669  isprm3  16670  prmind2  16672  maxprmfct  16696  prmdvdsexp  16702  pcmpt  16880  prmreclem4  16907  vdwmc2  16967  vdwlem10  16978  ramub2  17002  ramcl  17017  prmgaplem5  17043  prmgaplem8  17046  cshwshashlem1  17084  cshwshashlem3  17086  setsn0fun  17161  imasleval  17542  divsfval  17548  mreexexlem4d  17646  isssc  17822  initoeu1  18019  termoeu1  18026  istos  18429  mgmcl  18622  sgrpidmnd  18718  frmdgsum  18838  smndex1mgm  18883  dfgrp3lem  19018  mhmmulg  19095  resghm2b  19214  gsumwrev  19349  elsymgbas  19357  symgextf1  19405  gsmsymgreqlem2  19415  gsmsymgreq  19416  odlem1  19519  odcl2  19549  gexlem1  19563  efgi2  19709  efginvrel2  19711  efgsrel  19718  cyggexb  19883  gsummulglem  19925  gsumzunsnd  19940  gsum2dlem2  19955  telgsums  19977  dmdprd  19984  dprdw  19996  ablfac1eulem  20058  srgpcomp  20187  rnghmmul  20417  nrhmzr  20503  lmodfopnelem1  20810  rmodislmodlem  20841  cnfldmulg  21365  cnfldexp  21366  nzerooringczr  21440  obslbs  21698  mplcoe1  22014  mplcoe3  22015  mplcoe5  22017  cply1mul  22257  coe1fzgsumdlem  22264  gsummoncoe1  22269  pf1ind  22316  evl1gsumdlem  22317  mat1dimcrng  22440  ma1repveval  22534  mulmarep1gsum2  22537  gsummatr01lem3  22620  cramerlem3  22652  decpmatmulsumfsupp  22736  mp2pm2mplem4  22772  pm2mpmhmlem1  22781  fvmptnn04if  22812  cayhamlem1  22829  fctop  22968  mretopd  23057  restopnb  23140  restdis  23143  tgcnp  23218  cncls2  23238  cncls  23239  cnntr  23240  cnsscnp  23244  cmpsub  23365  2ndcsep  23424  1stcelcls  23426  lfinpfin  23489  locfincmp  23491  comppfsc  23497  txcn  23591  txlm  23613  xkohaus  23618  qtopres  23663  haushmphlem  23752  cmphmph  23753  connhmph  23754  reghmph  23758  nrmhmph  23759  ptcmpfi  23778  reghaus  23790  fbssfi  23802  fbun  23805  fbfinnfr  23806  isfildlem  23822  fgcl  23843  cfinfil  23858  supfil  23860  ufinffr  23894  fin1aufil  23897  cnpflf  23966  alexsubALTlem3  24014  alexsubALT  24016  cnextfvval  24030  cnextcn  24032  tmdgsum  24060  tgphaus  24082  tgpt1  24083  mettri  24319  blssexps  24393  blssex  24394  mopni3  24464  metss  24478  psmetutop  24537  dscmet  24542  tngngp3  24634  rectbntr0  24809  metnrmlem1a  24835  fsumcn  24849  lmmbr  25247  caubl  25297  caublcls  25298  bcthlem5  25317  bcth3  25320  ovolunlem1a  25486  ovoliunnul  25497  finiunmbl  25534  voliunlem1  25540  volsuplem  25545  volsup  25546  dyadmax  25588  itgfsum  25817  dvnadd  25920  cpnord  25926  dvnfre  25945  dvmptfsum  25968  dvlip  25987  fta1g  26166  plyco  26237  dgrcolem1  26270  dgrco  26272  dvnply2  26284  plydivex  26294  plyexmo  26310  aannenlem1  26325  aaliou3lem2  26340  dvntaylp  26368  taylthlem1  26370  ulmval  26378  cxpmul2  26685  cxpsqrtth  26726  scvxcvx  26983  jensenlem2  26985  jensen  26986  ppiub  27202  bcmono  27275  bpos1lem  27280  bposlem5  27286  gausslemma2dlem6  27370  lgsquad2lem2  27383  2lgslem3  27402  2lgs  27405  2sqnn  27437  addsqnreup  27441  2sqreultblem  27446  2sqreunnltblem  27449  dchrisumlem1  27487  dchrisum0flb  27508  pntpbnd1  27584  pntlemf  27603  qabvle  27623  qabvexp  27624  ostthlem2  27626  ostth2lem2  27632  sltval2  27655  sltsolem1  27674  negsprop  28013  mulsuniflem  28119  precsexlem6  28180  precsexlem7  28181  noseqind  28235  om2noseqlt  28242  n0addscl  28282  n0mulscl  28283  axeuclidlem  28865  axcontlem12  28878  umgrnloopv  29011  uhgredgrnv  29035  edglnl  29048  numedglnl  29049  usgruspgrb  29088  usgrnloopvALT  29106  usgredg2vlem2  29131  subupgr  29192  nbumgr  29252  uhgrnbgr0nb  29259  nbgr0edglem  29261  edgusgrnbfin  29278  nb3grprlem2  29286  uvtxnbgrvtx  29298  cplgrop  29342  cusgrfi  29364  fusgrmaxsize  29370  fusgrn0degnn0  29405  ewlkprop  29509  uspgr2wlkeq  29552  g0wlk0  29558  wlkreslem  29575  lfgriswlk  29594  upgrwlkdvde  29643  spthonepeq  29658  uhgrwkspth  29661  usgr2trlncl  29666  usgr2trlspth  29667  cyclnspth  29706  crctcshwlkn0lem3  29715  wwlksn  29740  wspthneq1eq2  29763  wwlksm1edg  29784  wwlksnred  29795  wwlksnextfun  29801  wwlksnextinj  29802  wwlksnextproplem3  29814  wspthsnonn0vne  29820  wspn0  29827  rusgrnumwwlk  29878  clwwlkccatlem  29891  umgrclwwlkge2  29893  clwlkclwwlklem2  29902  clwlkclwwlklem3  29903  clwwisshclwws  29917  clwwisshclwwsn  29918  clwwlkn1loopb  29945  wwlksext2clwwlk  29959  wwlksubclwwlk  29960  clwwlknonex2lem2  30010  upgr3v3e3cycl  30082  uhgr3cyclex  30084  upgr4cycl4dv4e  30087  eupth2lem3lem4  30133  eupth2lem3lem7  30136  eupth2  30141  eulerpath  30143  nfrgr2v  30174  frgr3vlem1  30175  3vfriswmgr  30180  1to2vfriswmgr  30181  1to3vfriswmgr  30182  3cyclfrgrrn1  30187  3cyclfrgrrn  30188  3cyclfrgrrn2  30189  4cycl2vnunb  30192  frgrncvvdeqlem2  30202  frgrncvvdeqlem8  30208  frgrncvvdeqlem9  30209  frgrwopreglem4a  30212  frgrwopreglem5lem  30222  frgrwopreglem5ALT  30224  frgrregorufr0  30226  frgr2wwlk1  30231  frgr2wwlkeqm  30233  fusgr2wsp2nb  30236  2wspmdisj  30239  frrusgrord  30243  numclwwlk1lem2f1  30259  numclwlk1  30273  frgrreggt1  30295  friendshipgt3  30300  hlim2  31094  elnlfn  31830  stle0i  32141  hstrbi  32168  spansncv2  32195  h1da  32251  fmptcof2  32544  xreceu  32751  domnprodn0  33086  1arithufdlem3  33379  1arithufdlem4  33380  tpr2rico  33664  hasheuni  33855  ismeas  33969  sseqp1  34166  rrvsum  34225  dstfrvunirn  34245  sgn3da  34312  signstfvc  34357  bnj607  34698  bnj1145  34775  bnj1204  34794  fineqvrep  34866  fisshasheq  34875  subgrwlk  34893  subfacp1lem6  34946  cvmlift2lem12  35075  cvmlift3lem4  35083  satfrnmapom  35131  sat1el2xp  35140  satffunlem2  35169  satffun  35170  mrsubvrs  35283  climuzcnv  35426  iprodefisumlem  35485  dfon2lem9  35538  linethru  35900  elhf2  35922  finminlem  35953  fnessref  35992  neibastop2lem  35995  fnemeet2  36002  nndivsub  36092  bj-xpnzex  36589  bj-elpwg  36682  bj-epelg  36698  mptsnunlem  36968  dissneqlem  36970  topdifinffinlem  36977  iooelexlt  36992  domalom  37034  fvineqsneq  37042  wl-exeq  37152  wl-ax11-lem3  37205  matunitlindflem1  37240  poimirlem22  37266  poimirlem26  37270  poimirlem28  37272  poimirlem29  37273  poimirlem32  37276  heicant  37279  ovoliunnfl  37286  voliunnfl  37288  volsupnfl  37289  cover2  37339  upixp  37353  sdclem2  37366  fdc  37369  seqpo  37371  metf1o  37379  mettrifi  37381  sstotbnd3  37400  heibor1lem  37433  heiborlem5  37439  heibor  37445  bfplem1  37446  elghomlem2OLD  37510  grpokerinj  37517  isrngo  37521  rngodm1dm2  37556  ispridl2  37662  exlimddvf  37745  lssatle  38637  4atexlemex4  39696  uzindd  41599  evl1gprodd  41739  sn-axprlem3  41858  mzpsubst  42315  jm2.18  42556  wepwsolem  42613  oaabsb  42870  oacl2g  42906  ofoafg  42930  ofoaid1  42934  ofoaid2  42935  naddonnn  42972  iunrelexp0  43279  relexpmulg  43287  cnvtrclfv  43301  clsk1indlem3  43620  grucollcld  43844  inaex  43881  dvgrat  43896  radcnvrat  43898  csbxpgVD  44480  sineq0ALT  44523  islptre  45150  iblspltprt  45504  stoweidlem2  45533  stoweidlem17  45548  stoweidlem21  45552  2reuimp0  46637  2reuimp  46638  afveu  46676  funbrafv  46681  ndmaovass  46729  afv2eu  46761  tz6.12c-afv2  46765  funop1  46806  f1oresf1o2  46814  fvmptrabdm  46816  nltle2tri  46836  2elfz2melfz  46841  fsummsndifre  46854  fsumsplitsndif  46855  fsummmodsndifre  46856  fsummmodsnunz  46857  elsetpreimafvssdm  46868  uniimaelsetpreimafv  46878  imasetpreimafvbijlemfv1  46885  iccpartiltu  46904  iccpartigtl  46905  iccpartleu  46910  iccpartgel  46911  iccpartrn  46912  iccpartiun  46916  icceuelpart  46918  iccpartnel  46920  fargshiftf  46922  fargshiftf1  46923  ichnfb  46947  elsprel  46957  prsprel  46969  sprsymrelfo  46979  paireqne  46993  sbcpr  47003  reupr  47004  fmtnoinf  47018  odz2prm2pw  47045  lighneallem4  47092  lighneal  47093  requad1  47104  requad2  47105  evensumeven  47189  even3prm2  47201  gbowgt5  47244  nnsum4primeseven  47282  nnsum4primesevenALTV  47283  bgoldbnnsum3prm  47286  bgoldbtbndlem2  47288  bgoldbtbndlem4  47290  bgoldbtbnd  47291  dfsclnbgr6  47335  uspgrimprop  47362  grimco  47369  clcllaw  47444  rngccatidALTV  47525  ringccatidALTV  47559  scmsuppss  47627  gsumlsscl  47638  ply1mulgsumlem2  47646  lincvalsc0  47680  linc0scn0  47682  lincdifsn  47683  linc1  47684  lincellss  47685  lincsum  47688  lincscm  47689  lincsumcl  47690  lcoss  47695  lincext3  47715  lindslinindimp2lem4  47720  lindslinindsimp2lem5  47721  lindslinindsimp2  47722  lindsrng01  47727  snlindsntor  47730  lincresunit3lem2  47739  lincresunit3  47740  islindeps2  47742  blengt1fldiv2p1  47857  2arymaptf1  47917  resum2sqorgt0  47973  reorelicc  47974  rrx2plordisom  47987  rrx2linest  48006  rrxsphere  48012  line2ylem  48015  itsclc0xyqsol  48032  itscnhlinecirc02p  48049  mo0sn  48077  thincn0eu  48229