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  2096  mo4  2560  2moswapv  2623  2moswap  2638  2mosOLD  2644  2eu2  2647  pm2.61ne  3011  nelelne  3025  r19.21be  3231  cbvraldva2  3323  rspcebdv  3585  2reu2  3864  csbie2df  4409  minel  4432  uneqdifeq  4459  raltpd  4748  ssunsn2  4794  opthprneg  4832  ssuni  4899  uniss2  4908  elpwuni  5072  intss2  5075  disjord  5099  elpw2g  5291  elssabg  5301  axprlem3OLD  5386  axprlem4OLD  5387  axprlem5OLD  5388  oteqex  5463  otsndisj  5482  otiunsndisj  5483  epelg  5542  wereu  5637  relop  5817  riinint  5938  sotri3  6106  unixpid  6260  reuop  6269  ordtr2  6380  ordsssuc2  6428  iotan0  6504  funopg  6553  fun  6725  tz6.12cOLD  6888  fvmptnf  6993  fvn0ssdmfun  7049  eldmrexrnb  7067  fmptco  7104  fnressn  7133  fressnfv  7135  fprb  7171  fvtp2g  7176  fvtp3g  7177  fconst2g  7180  fntpb  7186  f1dom3el3dif  7247  f1ounsn  7250  isores3  7313  isoselem  7319  oprabv  7452  eloprabga  7501  sorpsscmpl  7713  difex2  7739  ordpwsuc  7793  ordsucun  7803  limuni3  7831  trom  7854  fo1stres  7997  poxp  8110  soxp  8111  xpord3inddlem  8136  soseq  8141  suppimacnv  8156  fsuppeq  8157  funsssuppss  8172  brtpos2  8214  frrlem8  8275  fpr2a  8284  onnseq  8316  smores  8324  smofvon2  8328  tfrlem1  8347  oacl  8502  omcl  8503  oecl  8504  oawordri  8517  oalimcl  8527  oaass  8528  oarec  8529  omwordri  8539  omeulem1  8549  omeulem2  8550  oeordi  8554  oeworde  8560  oeoelem  8565  nnacl  8578  nnmcl  8579  nnecl  8580  nnacom  8584  nnaass  8589  nnmsucr  8592  nnmordi  8598  omabs  8618  cofonr  8641  naddunif  8660  iiner  8765  elpmg  8819  fsetfcdm  8836  fsetprcnex  8838  pmss12g  8845  mapfvd  8855  f1domg  8946  ssdomg  8974  undom  9033  domtriord  9093  ssnnfi  9139  fnfi  9148  enfi  9157  php  9177  sdom1  9196  1sdom2dom  9201  1sdomOLD  9203  fisseneq  9211  isinf  9214  isinfOLD  9215  dif1ennnALT  9229  findcard3  9236  findcard3OLD  9237  frfi  9239  difinf  9267  imafiOLD  9272  iunfi  9301  fsuppunfi  9346  fsuppres  9351  ffsuppbi  9356  elfi2  9372  marypha1lem  9391  marypha1  9392  oiexg  9495  wemapso2  9513  harword  9523  brwdom  9527  unxpwdom  9549  en3lplem1  9572  inf3lemd  9587  inf3lem5  9592  cantnfval2  9629  cantnfle  9631  cantnflt  9632  cnfcom  9660  tcmin  9701  frr2  9720  r1sdom  9734  rankxplim3  9841  cardidm  9919  cardmin2  9959  infxpenlem  9973  fseqenlem1  9984  numacn  10009  alephordi  10034  iscard3  10053  alephinit  10055  carduniima  10056  iunfictbso  10074  dfac5  10089  dfac12lem3  10106  nnadju  10158  pwsdompw  10163  pwdjudom  10175  cflim2  10223  cfslb2n  10228  cofsmo  10229  cfsmolem  10230  cfcoflem  10232  alephsing  10236  infpssALT  10273  fin23lem34  10306  isf32lem2  10314  isf32lem10  10322  isf32lem12  10324  isfin1-2  10345  hsmexlem4  10389  axcc2lem  10396  domtriomlem  10402  axdc2lem  10408  axdc3lem2  10411  axdc3lem4  10413  axdc4lem  10415  axcclem  10417  ac6num  10439  ac6s  10444  zorn2lem7  10462  ttukeylem5  10473  imadomg  10494  iundom2g  10500  ondomon  10523  ficard  10525  konigthlem  10528  alephreg  10542  pwcfsdom  10543  cfpwsdom  10544  axregndlem1  10562  axregnd  10564  pwfseqlem3  10620  pwxpndom2  10625  pwxpndom  10626  pwdjundom  10627  inawinalem  10649  gchina  10659  wuncval2  10707  tsk0  10723  tskxpss  10732  inatsk  10738  tskuni  10743  gruina  10778  grothac  10790  addclpi  10852  addnidpi  10861  nqereu  10889  mulcanenq  10920  genpnnp  10965  nqpr  10974  prlem934  10993  reclem2pr  11008  suplem1pr  11012  supsrlem  11071  axpre-sup  11129  1re  11181  dedekindle  11345  00id  11356  receu  11830  sup3  12147  infrelb  12175  peano5nni  12196  nnindd  12213  nnaddcl  12216  zrevaddcl  12585  nzadd  12588  zdiv  12611  nneo  12625  zeo2  12628  nn0indd  12638  fzind  12639  fnn0ind  12640  fzindd  12643  uzwo  12877  lbzbi  12902  nn01to3  12907  qrevaddcl  12937  irradd  12939  irrmul  12940  ltsubrp  12996  ltaddrp  12997  xnn0xaddcl  13202  xnn0xadd0  13214  icoshft  13441  fzen  13509  elfzm11  13563  uzsplit  13564  elfzom1elp1fzo  13700  fzoopth  13730  injresinjlem  13755  injresinj  13756  modifeq2int  13905  modsumfzodifsn  13916  om2uzlti  13922  ssnn0fi  13957  fsuppmapnn0fiub0  13965  mptnn0fsuppr  13971  seqcaopr3  14009  seqf1olem2a  14012  seqf1o  14015  ser1const  14030  expadd  14076  expmul  14079  leexp1a  14147  faccl  14255  facdiv  14259  faclbnd  14262  faclbnd4lem4  14268  hasheqf1oi  14323  hashgadd  14349  hashinfxadd  14357  hashunx  14358  hashunsng  14364  elprchashprn2  14368  hashss  14381  hash1snb  14391  hashmap  14407  hashf1lem2  14428  hashf1  14429  seqcoll  14436  hashle2pr  14449  hashdmpropge2  14455  hashge3el3dif  14459  hash1to3  14464  fundmge2nop0  14474  fi1uzind  14479  brfi1indALT  14482  sswrd  14494  swrdnd2  14627  swrdnnn0nd  14628  swrdnd0  14629  swrdwrdsymb  14634  pfxnd0  14660  swrdswrdlem  14676  swrdswrd  14677  wrd2ind  14695  swrdccatin1  14697  swrdccatin2  14701  pfxccatin12lem2  14703  pfxccat3  14706  repsdf2  14750  repswswrd  14756  cshw0  14766  cshwcl  14770  cshwlen  14771  cshf1  14782  swrdco  14810  relexpsucnnl  15003  rtrclreclem3  15033  rtrclreclem4  15034  relexpindlem  15036  rtrclind  15038  shftlem  15041  caubnd  15332  reusq0  15438  rlimcld2  15551  o1dif  15603  climub  15635  climserle  15636  iseraltlem2  15656  sumss  15697  fsumzcl2  15712  fsummsnunz  15727  fsumsplitsnun  15728  fsum2d  15744  modfsummods  15766  fsumabs  15774  fsumrlim  15784  fsumo1  15785  fsumiun  15794  climcndslem1  15822  climcndslem2  15823  cvgrat  15856  clim2prod  15861  prodfn0  15867  prodfrec  15868  ntrivcvg  15870  prodmo  15909  fprodss  15921  fprodabs  15947  fprodn0  15952  fprod2d  15954  fprodefsum  16068  ruclem8  16212  ruclem9  16213  dvdsmod0  16235  dvds2ln  16266  dvdsaddre2b  16284  dvdslelem  16286  dvdsdivcl  16293  alzdvds  16297  mod2eq1n2dvds  16324  oddnn02np1  16325  nn0o1gt2  16358  nno  16359  sumeven  16364  sumodd  16365  pwp1fsum  16368  ndvdsadd  16387  bitsinv1  16419  sadcadd  16435  sadadd2  16437  saddisjlem  16441  smuval2  16459  smupvallem  16460  smu01lem  16462  smupval  16465  smueqlem  16467  smumullem  16469  gcddiv  16528  rplpwr  16535  nn0seqcvgd  16547  seq1st  16548  alginv  16552  algcvga  16556  algfx  16557  absprodnn  16595  isprm2  16659  isprm3  16660  prmind2  16662  maxprmfct  16686  prmdvdsexp  16692  pcmpt  16870  prmreclem4  16897  vdwmc2  16957  vdwlem10  16968  ramub2  16992  ramcl  17007  prmgaplem5  17033  prmgaplem8  17036  cshwshashlem1  17073  cshwshashlem3  17075  setsn0fun  17150  imasleval  17511  divsfval  17517  mreexexlem4d  17615  isssc  17789  initoeu1  17980  termoeu1  17987  istos  18384  mgmcl  18577  sgrpidmnd  18673  frmdgsum  18796  smndex1mgm  18841  dfgrp3lem  18977  mhmmulg  19054  resghm2b  19173  gsumwrev  19305  elsymgbas  19311  symgextf1  19358  gsmsymgreqlem2  19368  gsmsymgreq  19369  odlem1  19472  odcl2  19502  gexlem1  19516  efgi2  19662  efginvrel2  19664  efgsrel  19671  cyggexb  19836  gsummulglem  19878  gsumzunsnd  19893  gsum2dlem2  19908  telgsums  19930  dmdprd  19937  dprdw  19949  ablfac1eulem  20011  srgpcomp  20134  rnghmmul  20365  nrhmzr  20453  lmodfopnelem1  20811  rmodislmodlem  20842  cnfldmulg  21322  cnfldexp  21323  nzerooringczr  21397  obslbs  21646  mplcoe1  21951  mplcoe3  21952  mplcoe5  21954  cply1mul  22190  coe1fzgsumdlem  22197  gsummoncoe1  22202  pf1ind  22249  evl1gsumdlem  22250  mat1dimcrng  22371  ma1repveval  22465  mulmarep1gsum2  22468  gsummatr01lem3  22551  cramerlem3  22583  decpmatmulsumfsupp  22667  mp2pm2mplem4  22703  pm2mpmhmlem1  22712  fvmptnn04if  22743  cayhamlem1  22760  fctop  22898  mretopd  22986  restopnb  23069  restdis  23072  tgcnp  23147  cncls2  23167  cncls  23168  cnntr  23169  cnsscnp  23173  cmpsub  23294  2ndcsep  23353  1stcelcls  23355  lfinpfin  23418  locfincmp  23420  comppfsc  23426  txcn  23520  txlm  23542  xkohaus  23547  qtopres  23592  haushmphlem  23681  cmphmph  23682  connhmph  23683  reghmph  23687  nrmhmph  23688  ptcmpfi  23707  reghaus  23719  fbssfi  23731  fbun  23734  fbfinnfr  23735  isfildlem  23751  fgcl  23772  cfinfil  23787  supfil  23789  ufinffr  23823  fin1aufil  23826  cnpflf  23895  alexsubALTlem3  23943  alexsubALT  23945  cnextfvval  23959  cnextcn  23961  tmdgsum  23989  tgphaus  24011  tgpt1  24012  mettri  24247  blssexps  24321  blssex  24322  mopni3  24389  metss  24403  psmetutop  24462  dscmet  24467  tngngp3  24551  rectbntr0  24728  metnrmlem1a  24754  fsumcn  24768  lmmbr  25165  caubl  25215  caublcls  25216  bcthlem5  25235  bcth3  25238  ovolunlem1a  25404  ovoliunnul  25415  finiunmbl  25452  voliunlem1  25458  volsuplem  25463  volsup  25464  dyadmax  25506  itgfsum  25735  dvnadd  25838  cpnord  25844  dvnfre  25863  dvmptfsum  25886  dvlip  25905  fta1g  26082  plyco  26153  dgrcolem1  26186  dgrco  26188  dvnply2  26202  plydivex  26212  plyexmo  26228  aannenlem1  26243  aaliou3lem2  26258  dvntaylp  26286  taylthlem1  26288  ulmval  26296  cxpmul2  26605  cxpsqrtth  26646  scvxcvx  26903  jensenlem2  26905  jensen  26906  ppiub  27122  bcmono  27195  bpos1lem  27200  bposlem5  27206  gausslemma2dlem6  27290  lgsquad2lem2  27303  2lgslem3  27322  2lgs  27325  2sqnn  27357  addsqnreup  27361  2sqreultblem  27366  2sqreunnltblem  27369  dchrisumlem1  27407  dchrisum0flb  27428  pntpbnd1  27504  pntlemf  27523  qabvle  27543  qabvexp  27544  ostthlem2  27546  ostth2lem2  27552  sltval2  27575  sltsolem1  27594  negsprop  27948  mulsuniflem  28059  precsexlem6  28121  precsexlem7  28122  noseqind  28193  om2noseqlt  28200  n0addscl  28243  n0mulscl  28244  expsne0  28328  axeuclidlem  28896  axcontlem12  28909  umgrnloopv  29040  uhgredgrnv  29064  edglnl  29077  numedglnl  29078  usgruspgrb  29117  usgrnloopvALT  29135  usgredg2vlem2  29160  subupgr  29221  nbumgr  29281  uhgrnbgr0nb  29288  nbgr0edglem  29290  edgusgrnbfin  29307  nb3grprlem2  29315  uvtxnbgrvtx  29327  cplgrop  29371  cusgrfi  29393  fusgrmaxsize  29399  fusgrn0degnn0  29434  ewlkprop  29538  uspgr2wlkeq  29581  g0wlk0  29587  wlkreslem  29604  lfgriswlk  29623  upgrwlkdvde  29674  spthonepeq  29689  uhgrwkspth  29692  usgr2trlncl  29697  usgr2trlspth  29698  cyclnumvtx  29737  cyclnspth  29738  crctcshwlkn0lem3  29749  wwlksn  29774  wspthneq1eq2  29797  wwlksm1edg  29818  wwlksnred  29829  wwlksnextfun  29835  wwlksnextinj  29836  wwlksnextproplem3  29848  wspthsnonn0vne  29854  wspn0  29861  rusgrnumwwlk  29912  clwwlkccatlem  29925  umgrclwwlkge2  29927  clwlkclwwlklem2  29936  clwlkclwwlklem3  29937  clwwisshclwws  29951  clwwisshclwwsn  29952  clwwlkn1loopb  29979  wwlksext2clwwlk  29993  wwlksubclwwlk  29994  clwwlknonex2lem2  30044  upgr3v3e3cycl  30116  uhgr3cyclex  30118  upgr4cycl4dv4e  30121  eupth2lem3lem4  30167  eupth2lem3lem7  30170  eupth2  30175  eulerpath  30177  nfrgr2v  30208  frgr3vlem1  30209  3vfriswmgr  30214  1to2vfriswmgr  30215  1to3vfriswmgr  30216  3cyclfrgrrn1  30221  3cyclfrgrrn  30222  3cyclfrgrrn2  30223  4cycl2vnunb  30226  frgrncvvdeqlem2  30236  frgrncvvdeqlem8  30242  frgrncvvdeqlem9  30243  frgrwopreglem4a  30246  frgrwopreglem5lem  30256  frgrwopreglem5ALT  30258  frgrregorufr0  30260  frgr2wwlk1  30265  frgr2wwlkeqm  30267  fusgr2wsp2nb  30270  2wspmdisj  30273  frrusgrord  30277  numclwwlk1lem2f1  30293  numclwlk1  30307  frgrreggt1  30329  friendshipgt3  30334  hlim2  31128  elnlfn  31864  stle0i  32175  hstrbi  32202  spansncv2  32229  h1da  32285  fmptcof2  32588  sgn3da  32766  xreceu  32849  domnprodn0  33233  1arithufdlem3  33524  1arithufdlem4  33525  tpr2rico  33909  hasheuni  34082  ismeas  34196  sseqp1  34393  rrvsum  34452  dstfrvunirn  34473  signstfvc  34572  bnj607  34913  bnj1145  34990  bnj1204  35009  fineqvrep  35092  onvf1odlem4  35100  fisshasheq  35109  subgrwlk  35126  subfacp1lem6  35179  cvmlift2lem12  35308  cvmlift3lem4  35316  satfrnmapom  35364  sat1el2xp  35373  satffunlem2  35402  satffun  35403  mrsubvrs  35516  climuzcnv  35665  iprodefisumlem  35734  dfon2lem9  35786  linethru  36148  elhf2  36170  finminlem  36313  fnessref  36352  neibastop2lem  36355  fnemeet2  36362  nndivsub  36452  bj-xpnzex  36954  bj-elpwg  37047  bj-epelg  37063  mptsnunlem  37333  dissneqlem  37335  topdifinffinlem  37342  iooelexlt  37357  domalom  37399  fvineqsneq  37407  wl-exeq  37529  wl-ax11-lem3  37582  matunitlindflem1  37617  poimirlem22  37643  poimirlem26  37647  poimirlem28  37649  poimirlem29  37650  poimirlem32  37653  heicant  37656  ovoliunnfl  37663  voliunnfl  37665  volsupnfl  37666  cover2  37716  upixp  37730  sdclem2  37743  fdc  37746  seqpo  37748  metf1o  37756  mettrifi  37758  sstotbnd3  37777  heibor1lem  37810  heiborlem5  37816  heibor  37822  bfplem1  37823  elghomlem2OLD  37887  grpokerinj  37894  isrngo  37898  rngodm1dm2  37933  ispridl2  38039  exlimddvf  38122  lssatle  39015  4atexlemex4  40074  uzindd  41972  evl1gprodd  42112  sn-axprlem3  42212  redvmptabs  42355  sn-sup3d  42487  mzpsubst  42743  jm2.18  42984  wepwsolem  43038  oaabsb  43290  oacl2g  43326  ofoafg  43350  ofoaid1  43354  ofoaid2  43355  naddonnn  43391  iunrelexp0  43698  relexpmulg  43706  cnvtrclfv  43720  clsk1indlem3  44039  grucollcld  44256  inaex  44293  dvgrat  44308  radcnvrat  44310  csbxpgVD  44890  sineq0ALT  44933  trfr  44959  relwf  44964  pwclaxpow  44981  omssaxinf2  44985  islptre  45624  iblspltprt  45978  stoweidlem2  46007  stoweidlem17  46022  stoweidlem21  46026  2reuimp0  47119  2reuimp  47120  afveu  47158  funbrafv  47163  ndmaovass  47211  afv2eu  47243  tz6.12c-afv2  47247  funop1  47288  f1oresf1o2  47296  fvmptrabdm  47298  nltle2tri  47318  2elfz2melfz  47323  fsummsndifre  47377  fsumsplitsndif  47378  fsummmodsndifre  47379  fsummmodsnunz  47380  elsetpreimafvssdm  47391  uniimaelsetpreimafv  47401  imasetpreimafvbijlemfv1  47408  iccpartiltu  47427  iccpartigtl  47428  iccpartleu  47433  iccpartgel  47434  iccpartrn  47435  iccpartiun  47439  icceuelpart  47441  iccpartnel  47443  fargshiftf  47445  fargshiftf1  47446  ichnfb  47470  elsprel  47480  prsprel  47492  sprsymrelfo  47502  paireqne  47516  sbcpr  47526  reupr  47527  fmtnoinf  47541  odz2prm2pw  47568  lighneallem4  47615  lighneal  47616  requad1  47627  requad2  47628  evensumeven  47712  even3prm2  47724  gbowgt5  47767  nnsum4primeseven  47805  nnsum4primesevenALTV  47806  bgoldbnnsum3prm  47809  bgoldbtbndlem2  47811  bgoldbtbndlem4  47813  bgoldbtbnd  47814  dfsclnbgr6  47862  grimco  47893  cycl3grtri  47950  isubgr3stgrlem6  47974  gricgrlic  48014  gpgedgvtx0  48056  gpgprismgr4cycllem3  48091  pgnbgreunbgrlem5  48117  clcllaw  48183  rngccatidALTV  48264  ringccatidALTV  48298  scmsuppss  48363  gsumlsscl  48372  ply1mulgsumlem2  48380  lincvalsc0  48414  linc0scn0  48416  lincdifsn  48417  linc1  48418  lincellss  48419  lincsum  48422  lincscm  48423  lincsumcl  48424  lcoss  48429  lincext3  48449  lindslinindimp2lem4  48454  lindslinindsimp2lem5  48455  lindslinindsimp2  48456  lindsrng01  48461  snlindsntor  48464  lincresunit3lem2  48473  lincresunit3  48474  islindeps2  48476  blengt1fldiv2p1  48586  2arymaptf1  48646  resum2sqorgt0  48702  reorelicc  48703  rrx2plordisom  48716  rrx2linest  48735  rrxsphere  48741  line2ylem  48744  itsclc0xyqsol  48761  itscnhlinecirc02p  48778  mo0sn  48808  thincn0eu  49424