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  847  4casesdan  1042  dedlema  1046  dedlemb  1047  sbiedvw  2095  mo4  2566  2moswapv  2629  2moswap  2644  2mosOLD  2650  2eu2  2653  pm2.61ne  3027  nelelne  3041  r19.21be  3252  cbvraldva2  3348  rspcebdv  3616  2reu2  3898  csbie2df  4443  minel  4466  uneqdifeq  4493  raltpd  4781  ssunsn2  4827  opthprneg  4865  ssuni  4932  uniss2  4941  elpwuni  5105  intss2  5108  disjord  5132  elpw2g  5333  elssabg  5343  axprlem3OLD  5428  axprlem4OLD  5429  axprlem5OLD  5430  oteqex  5505  otsndisj  5524  otiunsndisj  5525  epelg  5585  wereu  5681  relop  5861  riinint  5982  sotri3  6150  unixpid  6304  reuop  6313  ordtr2  6428  ordsssuc2  6475  iotan0  6551  funopg  6600  fun  6770  tz6.12cOLD  6933  fvmptnf  7038  fvn0ssdmfun  7094  eldmrexrnb  7112  fmptco  7149  fnressn  7178  fressnfv  7180  fprb  7214  fvtp2g  7219  fvtp3g  7220  fconst2g  7223  fntpb  7229  f1dom3el3dif  7289  f1ounsn  7292  isores3  7355  isoselem  7361  oprabv  7493  eloprabga  7542  sorpsscmpl  7754  difex2  7780  ordpwsuc  7835  ordsucun  7845  limuni3  7873  trom  7896  fo1stres  8040  poxp  8153  soxp  8154  xpord3inddlem  8179  soseq  8184  suppimacnv  8199  fsuppeq  8200  funsssuppss  8215  brtpos2  8257  frrlem8  8318  fpr2a  8327  wfrlem12OLD  8360  onnseq  8384  smores  8392  smofvon2  8396  tfrlem1  8416  oacl  8573  omcl  8574  oecl  8575  oawordri  8588  oalimcl  8598  oaass  8599  oarec  8600  omwordri  8610  omeulem1  8620  omeulem2  8621  oeordi  8625  oeworde  8631  oeoelem  8636  nnacl  8649  nnmcl  8650  nnecl  8651  nnacom  8655  nnaass  8660  nnmsucr  8663  nnmordi  8669  omabs  8689  cofonr  8712  naddunif  8731  iiner  8829  elpmg  8883  fsetfcdm  8900  fsetprcnex  8902  pmss12g  8909  mapfvd  8919  f1domg  9012  ssdomg  9040  undom  9099  domtriord  9163  ssnnfi  9209  fnfi  9218  enfi  9227  php  9247  phpOLD  9259  php3OLD  9261  sdom1  9278  1sdom2dom  9283  1sdomOLD  9285  fisseneq  9293  isinf  9296  isinfOLD  9297  dif1ennnALT  9311  findcard3  9318  findcard3OLD  9319  frfi  9321  difinf  9349  imafiOLD  9354  iunfi  9383  fsuppunfi  9428  fsuppres  9433  ffsuppbi  9438  elfi2  9454  marypha1lem  9473  marypha1  9474  oiexg  9575  wemapso2  9593  harword  9603  brwdom  9607  unxpwdom  9629  en3lplem1  9652  inf3lemd  9667  inf3lem5  9672  cantnfval2  9709  cantnfle  9711  cantnflt  9712  cnfcom  9740  tcmin  9781  frr2  9800  r1sdom  9814  rankxplim3  9921  cardidm  9999  cardmin2  10039  infxpenlem  10053  fseqenlem1  10064  numacn  10089  alephordi  10114  iscard3  10133  alephinit  10135  carduniima  10136  iunfictbso  10154  dfac5  10169  dfac12lem3  10186  nnadju  10238  pwsdompw  10243  pwdjudom  10255  cflim2  10303  cfslb2n  10308  cofsmo  10309  cfsmolem  10310  cfcoflem  10312  alephsing  10316  infpssALT  10353  fin23lem34  10386  isf32lem2  10394  isf32lem10  10402  isf32lem12  10404  isfin1-2  10425  hsmexlem4  10469  axcc2lem  10476  domtriomlem  10482  axdc2lem  10488  axdc3lem2  10491  axdc3lem4  10493  axdc4lem  10495  axcclem  10497  ac6num  10519  ac6s  10524  zorn2lem7  10542  ttukeylem5  10553  imadomg  10574  iundom2g  10580  ondomon  10603  ficard  10605  konigthlem  10608  alephreg  10622  pwcfsdom  10623  cfpwsdom  10624  axregndlem1  10642  axregnd  10644  pwfseqlem3  10700  pwxpndom2  10705  pwxpndom  10706  pwdjundom  10707  inawinalem  10729  gchina  10739  wuncval2  10787  tsk0  10803  tskxpss  10812  inatsk  10818  tskuni  10823  gruina  10858  grothac  10870  addclpi  10932  addnidpi  10941  nqereu  10969  mulcanenq  11000  genpnnp  11045  nqpr  11054  prlem934  11073  reclem2pr  11088  suplem1pr  11092  supsrlem  11151  axpre-sup  11209  1re  11261  dedekindle  11425  00id  11436  receu  11908  sup3  12225  infrelb  12253  peano5nni  12269  nnindd  12286  nnaddcl  12289  zrevaddcl  12662  nzadd  12665  zdiv  12688  nneo  12702  zeo2  12705  nn0indd  12715  fzind  12716  fnn0ind  12717  fzindd  12720  uzwo  12953  lbzbi  12978  nn01to3  12983  qrevaddcl  13013  irradd  13015  irrmul  13016  ltsubrp  13071  ltaddrp  13072  xnn0xaddcl  13277  xnn0xadd0  13289  icoshft  13513  fzen  13581  elfzm11  13635  uzsplit  13636  elfzom1elp1fzo  13771  fzoopth  13801  injresinjlem  13826  injresinj  13827  modifeq2int  13974  modsumfzodifsn  13985  om2uzlti  13991  ssnn0fi  14026  fsuppmapnn0fiub0  14034  mptnn0fsuppr  14040  seqcaopr3  14078  seqf1olem2a  14081  seqf1o  14084  ser1const  14099  expadd  14145  expmul  14148  leexp1a  14215  faccl  14322  facdiv  14326  faclbnd  14329  faclbnd4lem4  14335  hasheqf1oi  14390  hashgadd  14416  hashinfxadd  14424  hashunx  14425  hashunsng  14431  elprchashprn2  14435  hashss  14448  hash1snb  14458  hashmap  14474  hashf1lem2  14495  hashf1  14496  seqcoll  14503  hashle2pr  14516  hashdmpropge2  14522  hashge3el3dif  14526  hash1to3  14531  fundmge2nop0  14541  fi1uzind  14546  brfi1indALT  14549  sswrd  14560  swrdnd2  14693  swrdnnn0nd  14694  swrdnd0  14695  swrdwrdsymb  14700  pfxnd0  14726  swrdswrdlem  14742  swrdswrd  14743  wrd2ind  14761  swrdccatin1  14763  swrdccatin2  14767  pfxccatin12lem2  14769  pfxccat3  14772  repsdf2  14816  repswswrd  14822  cshw0  14832  cshwcl  14836  cshwlen  14837  cshf1  14848  swrdco  14876  relexpsucnnl  15069  rtrclreclem3  15099  rtrclreclem4  15100  relexpindlem  15102  rtrclind  15104  shftlem  15107  caubnd  15397  reusq0  15501  rlimcld2  15614  o1dif  15666  climub  15698  climserle  15699  iseraltlem2  15719  sumss  15760  fsumzcl2  15775  fsummsnunz  15790  fsumsplitsnun  15791  fsum2d  15807  modfsummods  15829  fsumabs  15837  fsumrlim  15847  fsumo1  15848  fsumiun  15857  climcndslem1  15885  climcndslem2  15886  cvgrat  15919  clim2prod  15924  prodfn0  15930  prodfrec  15931  ntrivcvg  15933  prodmo  15972  fprodss  15984  fprodabs  16010  fprodn0  16015  fprod2d  16017  fprodefsum  16131  ruclem8  16273  ruclem9  16274  dvdsmod0  16296  dvds2ln  16326  dvdsaddre2b  16344  dvdslelem  16346  dvdsdivcl  16353  alzdvds  16357  mod2eq1n2dvds  16384  oddnn02np1  16385  nn0o1gt2  16418  nno  16419  sumeven  16424  sumodd  16425  pwp1fsum  16428  ndvdsadd  16447  bitsinv1  16479  sadcadd  16495  sadadd2  16497  saddisjlem  16501  smuval2  16519  smupvallem  16520  smu01lem  16522  smupval  16525  smueqlem  16527  smumullem  16529  gcddiv  16588  rplpwr  16595  nn0seqcvgd  16607  seq1st  16608  alginv  16612  algcvga  16616  algfx  16617  absprodnn  16655  isprm2  16719  isprm3  16720  prmind2  16722  maxprmfct  16746  prmdvdsexp  16752  pcmpt  16930  prmreclem4  16957  vdwmc2  17017  vdwlem10  17028  ramub2  17052  ramcl  17067  prmgaplem5  17093  prmgaplem8  17096  cshwshashlem1  17133  cshwshashlem3  17135  setsn0fun  17210  imasleval  17586  divsfval  17592  mreexexlem4d  17690  isssc  17864  initoeu1  18056  termoeu1  18063  istos  18463  mgmcl  18656  sgrpidmnd  18752  frmdgsum  18875  smndex1mgm  18920  dfgrp3lem  19056  mhmmulg  19133  resghm2b  19252  gsumwrev  19385  elsymgbas  19391  symgextf1  19439  gsmsymgreqlem2  19449  gsmsymgreq  19450  odlem1  19553  odcl2  19583  gexlem1  19597  efgi2  19743  efginvrel2  19745  efgsrel  19752  cyggexb  19917  gsummulglem  19959  gsumzunsnd  19974  gsum2dlem2  19989  telgsums  20011  dmdprd  20018  dprdw  20030  ablfac1eulem  20092  srgpcomp  20215  rnghmmul  20449  nrhmzr  20537  lmodfopnelem1  20896  rmodislmodlem  20927  cnfldmulg  21416  cnfldexp  21417  nzerooringczr  21491  obslbs  21750  mplcoe1  22055  mplcoe3  22056  mplcoe5  22058  cply1mul  22300  coe1fzgsumdlem  22307  gsummoncoe1  22312  pf1ind  22359  evl1gsumdlem  22360  mat1dimcrng  22483  ma1repveval  22577  mulmarep1gsum2  22580  gsummatr01lem3  22663  cramerlem3  22695  decpmatmulsumfsupp  22779  mp2pm2mplem4  22815  pm2mpmhmlem1  22824  fvmptnn04if  22855  cayhamlem1  22872  fctop  23011  mretopd  23100  restopnb  23183  restdis  23186  tgcnp  23261  cncls2  23281  cncls  23282  cnntr  23283  cnsscnp  23287  cmpsub  23408  2ndcsep  23467  1stcelcls  23469  lfinpfin  23532  locfincmp  23534  comppfsc  23540  txcn  23634  txlm  23656  xkohaus  23661  qtopres  23706  haushmphlem  23795  cmphmph  23796  connhmph  23797  reghmph  23801  nrmhmph  23802  ptcmpfi  23821  reghaus  23833  fbssfi  23845  fbun  23848  fbfinnfr  23849  isfildlem  23865  fgcl  23886  cfinfil  23901  supfil  23903  ufinffr  23937  fin1aufil  23940  cnpflf  24009  alexsubALTlem3  24057  alexsubALT  24059  cnextfvval  24073  cnextcn  24075  tmdgsum  24103  tgphaus  24125  tgpt1  24126  mettri  24362  blssexps  24436  blssex  24437  mopni3  24507  metss  24521  psmetutop  24580  dscmet  24585  tngngp3  24677  rectbntr0  24854  metnrmlem1a  24880  fsumcn  24894  lmmbr  25292  caubl  25342  caublcls  25343  bcthlem5  25362  bcth3  25365  ovolunlem1a  25531  ovoliunnul  25542  finiunmbl  25579  voliunlem1  25585  volsuplem  25590  volsup  25591  dyadmax  25633  itgfsum  25862  dvnadd  25965  cpnord  25971  dvnfre  25990  dvmptfsum  26013  dvlip  26032  fta1g  26209  plyco  26280  dgrcolem1  26313  dgrco  26315  dvnply2  26329  plydivex  26339  plyexmo  26355  aannenlem1  26370  aaliou3lem2  26385  dvntaylp  26413  taylthlem1  26415  ulmval  26423  cxpmul2  26731  cxpsqrtth  26772  scvxcvx  27029  jensenlem2  27031  jensen  27032  ppiub  27248  bcmono  27321  bpos1lem  27326  bposlem5  27332  gausslemma2dlem6  27416  lgsquad2lem2  27429  2lgslem3  27448  2lgs  27451  2sqnn  27483  addsqnreup  27487  2sqreultblem  27492  2sqreunnltblem  27495  dchrisumlem1  27533  dchrisum0flb  27554  pntpbnd1  27630  pntlemf  27649  qabvle  27669  qabvexp  27670  ostthlem2  27672  ostth2lem2  27678  sltval2  27701  sltsolem1  27720  negsprop  28067  mulsuniflem  28175  precsexlem6  28236  precsexlem7  28237  noseqind  28298  om2noseqlt  28305  n0addscl  28347  n0mulscl  28348  expsne0  28414  axeuclidlem  28977  axcontlem12  28990  umgrnloopv  29123  uhgredgrnv  29147  edglnl  29160  numedglnl  29161  usgruspgrb  29200  usgrnloopvALT  29218  usgredg2vlem2  29243  subupgr  29304  nbumgr  29364  uhgrnbgr0nb  29371  nbgr0edglem  29373  edgusgrnbfin  29390  nb3grprlem2  29398  uvtxnbgrvtx  29410  cplgrop  29454  cusgrfi  29476  fusgrmaxsize  29482  fusgrn0degnn0  29517  ewlkprop  29621  uspgr2wlkeq  29664  g0wlk0  29670  wlkreslem  29687  lfgriswlk  29706  upgrwlkdvde  29757  spthonepeq  29772  uhgrwkspth  29775  usgr2trlncl  29780  usgr2trlspth  29781  cyclnumvtx  29820  cyclnspth  29821  crctcshwlkn0lem3  29832  wwlksn  29857  wspthneq1eq2  29880  wwlksm1edg  29901  wwlksnred  29912  wwlksnextfun  29918  wwlksnextinj  29919  wwlksnextproplem3  29931  wspthsnonn0vne  29937  wspn0  29944  rusgrnumwwlk  29995  clwwlkccatlem  30008  umgrclwwlkge2  30010  clwlkclwwlklem2  30019  clwlkclwwlklem3  30020  clwwisshclwws  30034  clwwisshclwwsn  30035  clwwlkn1loopb  30062  wwlksext2clwwlk  30076  wwlksubclwwlk  30077  clwwlknonex2lem2  30127  upgr3v3e3cycl  30199  uhgr3cyclex  30201  upgr4cycl4dv4e  30204  eupth2lem3lem4  30250  eupth2lem3lem7  30253  eupth2  30258  eulerpath  30260  nfrgr2v  30291  frgr3vlem1  30292  3vfriswmgr  30297  1to2vfriswmgr  30298  1to3vfriswmgr  30299  3cyclfrgrrn1  30304  3cyclfrgrrn  30305  3cyclfrgrrn2  30306  4cycl2vnunb  30309  frgrncvvdeqlem2  30319  frgrncvvdeqlem8  30325  frgrncvvdeqlem9  30326  frgrwopreglem4a  30329  frgrwopreglem5lem  30339  frgrwopreglem5ALT  30341  frgrregorufr0  30343  frgr2wwlk1  30348  frgr2wwlkeqm  30350  fusgr2wsp2nb  30353  2wspmdisj  30356  frrusgrord  30360  numclwwlk1lem2f1  30376  numclwlk1  30390  frgrreggt1  30412  friendshipgt3  30417  hlim2  31211  elnlfn  31947  stle0i  32258  hstrbi  32285  spansncv2  32312  h1da  32368  fmptcof2  32667  xreceu  32904  domnprodn0  33279  1arithufdlem3  33574  1arithufdlem4  33575  tpr2rico  33911  hasheuni  34086  ismeas  34200  sseqp1  34397  rrvsum  34456  dstfrvunirn  34477  sgn3da  34544  signstfvc  34589  bnj607  34930  bnj1145  35007  bnj1204  35026  fineqvrep  35109  fisshasheq  35120  subgrwlk  35137  subfacp1lem6  35190  cvmlift2lem12  35319  cvmlift3lem4  35327  satfrnmapom  35375  sat1el2xp  35384  satffunlem2  35413  satffun  35414  mrsubvrs  35527  climuzcnv  35676  iprodefisumlem  35740  dfon2lem9  35792  linethru  36154  elhf2  36176  finminlem  36319  fnessref  36358  neibastop2lem  36361  fnemeet2  36368  nndivsub  36458  bj-xpnzex  36960  bj-elpwg  37053  bj-epelg  37069  mptsnunlem  37339  dissneqlem  37341  topdifinffinlem  37348  iooelexlt  37363  domalom  37405  fvineqsneq  37413  wl-exeq  37535  wl-ax11-lem3  37588  matunitlindflem1  37623  poimirlem22  37649  poimirlem26  37653  poimirlem28  37655  poimirlem29  37656  poimirlem32  37659  heicant  37662  ovoliunnfl  37669  voliunnfl  37671  volsupnfl  37672  cover2  37722  upixp  37736  sdclem2  37749  fdc  37752  seqpo  37754  metf1o  37762  mettrifi  37764  sstotbnd3  37783  heibor1lem  37816  heiborlem5  37822  heibor  37828  bfplem1  37829  elghomlem2OLD  37893  grpokerinj  37900  isrngo  37904  rngodm1dm2  37939  ispridl2  38045  exlimddvf  38128  lssatle  39016  4atexlemex4  40075  uzindd  41978  evl1gprodd  42118  sn-axprlem3  42256  redvmptabs  42390  sn-sup3d  42502  mzpsubst  42759  jm2.18  43000  wepwsolem  43054  oaabsb  43307  oacl2g  43343  ofoafg  43367  ofoaid1  43371  ofoaid2  43372  naddonnn  43408  iunrelexp0  43715  relexpmulg  43723  cnvtrclfv  43737  clsk1indlem3  44056  grucollcld  44279  inaex  44316  dvgrat  44331  radcnvrat  44333  csbxpgVD  44914  sineq0ALT  44957  trfr  44979  relwf  44984  pwclaxpow  45001  omssaxinf2  45005  islptre  45634  iblspltprt  45988  stoweidlem2  46017  stoweidlem17  46032  stoweidlem21  46036  2reuimp0  47126  2reuimp  47127  afveu  47165  funbrafv  47170  ndmaovass  47218  afv2eu  47250  tz6.12c-afv2  47254  funop1  47295  f1oresf1o2  47303  fvmptrabdm  47305  nltle2tri  47325  2elfz2melfz  47330  fsummsndifre  47359  fsumsplitsndif  47360  fsummmodsndifre  47361  fsummmodsnunz  47362  elsetpreimafvssdm  47373  uniimaelsetpreimafv  47383  imasetpreimafvbijlemfv1  47390  iccpartiltu  47409  iccpartigtl  47410  iccpartleu  47415  iccpartgel  47416  iccpartrn  47417  iccpartiun  47421  icceuelpart  47423  iccpartnel  47425  fargshiftf  47427  fargshiftf1  47428  ichnfb  47452  elsprel  47462  prsprel  47474  sprsymrelfo  47484  paireqne  47498  sbcpr  47508  reupr  47509  fmtnoinf  47523  odz2prm2pw  47550  lighneallem4  47597  lighneal  47598  requad1  47609  requad2  47610  evensumeven  47694  even3prm2  47706  gbowgt5  47749  nnsum4primeseven  47787  nnsum4primesevenALTV  47788  bgoldbnnsum3prm  47791  bgoldbtbndlem2  47793  bgoldbtbndlem4  47795  bgoldbtbnd  47796  dfsclnbgr6  47844  uspgrimprop  47873  grimco  47880  cycl3grtri  47914  isubgr3stgrlem6  47938  gricgrlic  47978  gpgedgvtx0  48019  clcllaw  48107  rngccatidALTV  48188  ringccatidALTV  48222  scmsuppss  48287  gsumlsscl  48296  ply1mulgsumlem2  48304  lincvalsc0  48338  linc0scn0  48340  lincdifsn  48341  linc1  48342  lincellss  48343  lincsum  48346  lincscm  48347  lincsumcl  48348  lcoss  48353  lincext3  48373  lindslinindimp2lem4  48378  lindslinindsimp2lem5  48379  lindslinindsimp2  48380  lindsrng01  48385  snlindsntor  48388  lincresunit3lem2  48397  lincresunit3  48398  islindeps2  48400  blengt1fldiv2p1  48514  2arymaptf1  48574  resum2sqorgt0  48630  reorelicc  48631  rrx2plordisom  48644  rrx2linest  48663  rrxsphere  48669  line2ylem  48672  itsclc0xyqsol  48689  itscnhlinecirc02p  48706  mo0sn  48735  thincn0eu  49080