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  2092  mo4  2563  2moswapv  2626  2moswap  2641  2mosOLD  2647  2eu2  2650  pm2.61ne  3024  nelelne  3038  r19.21be  3249  cbvraldva2  3345  rspcebdv  3615  2reu2  3906  csbie2df  4448  minel  4471  uneqdifeq  4498  raltpd  4785  ssunsn2  4831  opthprneg  4869  ssuni  4936  uniss2  4945  elpwuni  5109  intss2  5112  disjord  5136  elpw2g  5338  elssabg  5348  axprlem3OLD  5433  axprlem4OLD  5434  axprlem5OLD  5435  oteqex  5509  otsndisj  5528  otiunsndisj  5529  epelg  5589  wereu  5684  relop  5863  riinint  5984  sotri3  6152  unixpid  6305  reuop  6314  ordtr2  6429  ordsssuc2  6476  iotan0  6552  funopg  6601  fun  6770  tz6.12cOLD  6933  fvmptnf  7037  fvn0ssdmfun  7093  eldmrexrnb  7111  fmptco  7148  fnressn  7177  fressnfv  7179  fprb  7213  fvtp2g  7218  fvtp3g  7219  fconst2g  7222  fntpb  7228  f1dom3el3dif  7288  f1ounsn  7291  isores3  7354  isoselem  7360  oprabv  7492  eloprabga  7540  eloprabgaOLD  7541  sorpsscmpl  7752  difex2  7778  ordpwsuc  7834  ordsucun  7844  limuni3  7872  trom  7895  fo1stres  8038  poxp  8151  soxp  8152  xpord3inddlem  8177  soseq  8182  suppimacnv  8197  fsuppeq  8198  funsssuppss  8213  brtpos2  8255  frrlem8  8316  fpr2a  8325  wfrlem12OLD  8358  onnseq  8382  smores  8390  smofvon2  8394  tfrlem1  8414  oacl  8571  omcl  8572  oecl  8573  oawordri  8586  oalimcl  8596  oaass  8597  oarec  8598  omwordri  8608  omeulem1  8618  omeulem2  8619  oeordi  8623  oeworde  8629  oeoelem  8634  nnacl  8647  nnmcl  8648  nnecl  8649  nnacom  8653  nnaass  8658  nnmsucr  8661  nnmordi  8667  omabs  8687  cofonr  8710  naddunif  8729  iiner  8827  elpmg  8881  fsetfcdm  8898  fsetprcnex  8900  pmss12g  8907  mapfvd  8917  f1domg  9010  ssdomg  9038  undom  9097  domtriord  9161  ssnnfi  9207  fnfi  9215  enfi  9224  php  9244  phpOLD  9256  php3OLD  9258  sdom1  9275  1sdom2dom  9280  1sdomOLD  9282  fisseneq  9290  isinf  9293  isinfOLD  9294  dif1ennnALT  9308  findcard3  9315  findcard3OLD  9316  frfi  9318  difinf  9346  imafiOLD  9351  iunfi  9380  fsuppunfi  9425  fsuppres  9430  ffsuppbi  9435  elfi2  9451  marypha1lem  9470  marypha1  9471  oiexg  9572  wemapso2  9590  harword  9600  brwdom  9604  unxpwdom  9626  en3lplem1  9649  inf3lemd  9664  inf3lem5  9669  cantnfval2  9706  cantnfle  9708  cantnflt  9709  cnfcom  9737  tcmin  9778  frr2  9797  r1sdom  9811  rankxplim3  9918  cardidm  9996  cardmin2  10036  infxpenlem  10050  fseqenlem1  10061  numacn  10086  alephordi  10111  iscard3  10130  alephinit  10132  carduniima  10133  iunfictbso  10151  dfac5  10166  dfac12lem3  10183  nnadju  10235  pwsdompw  10240  pwdjudom  10252  cflim2  10300  cfslb2n  10305  cofsmo  10306  cfsmolem  10307  cfcoflem  10309  alephsing  10313  infpssALT  10350  fin23lem34  10383  isf32lem2  10391  isf32lem10  10399  isf32lem12  10401  isfin1-2  10422  hsmexlem4  10466  axcc2lem  10473  domtriomlem  10479  axdc2lem  10485  axdc3lem2  10488  axdc3lem4  10490  axdc4lem  10492  axcclem  10494  ac6num  10516  ac6s  10521  zorn2lem7  10539  ttukeylem5  10550  imadomg  10571  iundom2g  10577  ondomon  10600  ficard  10602  konigthlem  10605  alephreg  10619  pwcfsdom  10620  cfpwsdom  10621  axregndlem1  10639  axregnd  10641  pwfseqlem3  10697  pwxpndom2  10702  pwxpndom  10703  pwdjundom  10704  inawinalem  10726  gchina  10736  wuncval2  10784  tsk0  10800  tskxpss  10809  inatsk  10815  tskuni  10820  gruina  10855  grothac  10867  addclpi  10929  addnidpi  10938  nqereu  10966  mulcanenq  10997  genpnnp  11042  nqpr  11051  prlem934  11070  reclem2pr  11085  suplem1pr  11089  supsrlem  11148  axpre-sup  11206  1re  11258  dedekindle  11422  00id  11433  receu  11905  sup3  12222  infrelb  12250  peano5nni  12266  nnindd  12283  nnaddcl  12286  zrevaddcl  12659  nzadd  12662  zdiv  12685  nneo  12699  zeo2  12702  nn0indd  12712  fzind  12713  fnn0ind  12714  fzindd  12717  uzwo  12950  lbzbi  12975  nn01to3  12980  qrevaddcl  13010  irradd  13012  irrmul  13013  ltsubrp  13068  ltaddrp  13069  xnn0xaddcl  13273  xnn0xadd0  13285  icoshft  13509  fzen  13577  elfzm11  13631  uzsplit  13632  elfzom1elp1fzo  13767  fzoopth  13797  injresinjlem  13822  injresinj  13823  modifeq2int  13970  modsumfzodifsn  13981  om2uzlti  13987  ssnn0fi  14022  fsuppmapnn0fiub0  14030  mptnn0fsuppr  14036  seqcaopr3  14074  seqf1olem2a  14077  seqf1o  14080  ser1const  14095  expadd  14141  expmul  14144  leexp1a  14211  faccl  14318  facdiv  14322  faclbnd  14325  faclbnd4lem4  14331  hasheqf1oi  14386  hashgadd  14412  hashinfxadd  14420  hashunx  14421  hashunsng  14427  elprchashprn2  14431  hashss  14444  hash1snb  14454  hashmap  14470  hashf1lem2  14491  hashf1  14492  seqcoll  14499  hashle2pr  14512  hashdmpropge2  14518  hashge3el3dif  14522  hash1to3  14527  fundmge2nop0  14537  fi1uzind  14542  brfi1indALT  14545  sswrd  14556  swrdnd2  14689  swrdnnn0nd  14690  swrdnd0  14691  swrdwrdsymb  14696  pfxnd0  14722  swrdswrdlem  14738  swrdswrd  14739  wrd2ind  14757  swrdccatin1  14759  swrdccatin2  14763  pfxccatin12lem2  14765  pfxccat3  14768  repsdf2  14812  repswswrd  14818  cshw0  14828  cshwcl  14832  cshwlen  14833  cshf1  14844  swrdco  14872  relexpsucnnl  15065  rtrclreclem3  15095  rtrclreclem4  15096  relexpindlem  15098  rtrclind  15100  shftlem  15103  caubnd  15393  reusq0  15497  rlimcld2  15610  o1dif  15662  climub  15694  climserle  15695  iseraltlem2  15715  sumss  15756  fsumzcl2  15771  fsummsnunz  15786  fsumsplitsnun  15787  fsum2d  15803  modfsummods  15825  fsumabs  15833  fsumrlim  15843  fsumo1  15844  fsumiun  15853  climcndslem1  15881  climcndslem2  15882  cvgrat  15915  clim2prod  15920  prodfn0  15926  prodfrec  15927  ntrivcvg  15929  prodmo  15968  fprodss  15980  fprodabs  16006  fprodn0  16011  fprod2d  16013  fprodefsum  16127  ruclem8  16269  ruclem9  16270  dvdsmod0  16292  dvds2ln  16322  dvdsaddre2b  16340  dvdslelem  16342  dvdsdivcl  16349  alzdvds  16353  mod2eq1n2dvds  16380  oddnn02np1  16381  nn0o1gt2  16414  nno  16415  sumeven  16420  sumodd  16421  pwp1fsum  16424  ndvdsadd  16443  bitsinv1  16475  sadcadd  16491  sadadd2  16493  saddisjlem  16497  smuval2  16515  smupvallem  16516  smu01lem  16518  smupval  16521  smueqlem  16523  smumullem  16525  gcddiv  16584  rplpwr  16591  nn0seqcvgd  16603  seq1st  16604  alginv  16608  algcvga  16612  algfx  16613  absprodnn  16651  isprm2  16715  isprm3  16716  prmind2  16718  maxprmfct  16742  prmdvdsexp  16748  pcmpt  16925  prmreclem4  16952  vdwmc2  17012  vdwlem10  17023  ramub2  17047  ramcl  17062  prmgaplem5  17088  prmgaplem8  17091  cshwshashlem1  17129  cshwshashlem3  17131  setsn0fun  17206  imasleval  17587  divsfval  17593  mreexexlem4d  17691  isssc  17867  initoeu1  18064  termoeu1  18071  istos  18475  mgmcl  18668  sgrpidmnd  18764  frmdgsum  18887  smndex1mgm  18932  dfgrp3lem  19068  mhmmulg  19145  resghm2b  19264  gsumwrev  19399  elsymgbas  19405  symgextf1  19453  gsmsymgreqlem2  19463  gsmsymgreq  19464  odlem1  19567  odcl2  19597  gexlem1  19611  efgi2  19757  efginvrel2  19759  efgsrel  19766  cyggexb  19931  gsummulglem  19973  gsumzunsnd  19988  gsum2dlem2  20003  telgsums  20025  dmdprd  20032  dprdw  20044  ablfac1eulem  20106  srgpcomp  20235  rnghmmul  20465  nrhmzr  20553  lmodfopnelem1  20912  rmodislmodlem  20943  cnfldmulg  21433  cnfldexp  21434  nzerooringczr  21508  obslbs  21767  mplcoe1  22072  mplcoe3  22073  mplcoe5  22075  cply1mul  22315  coe1fzgsumdlem  22322  gsummoncoe1  22327  pf1ind  22374  evl1gsumdlem  22375  mat1dimcrng  22498  ma1repveval  22592  mulmarep1gsum2  22595  gsummatr01lem3  22678  cramerlem3  22710  decpmatmulsumfsupp  22794  mp2pm2mplem4  22830  pm2mpmhmlem1  22839  fvmptnn04if  22870  cayhamlem1  22887  fctop  23026  mretopd  23115  restopnb  23198  restdis  23201  tgcnp  23276  cncls2  23296  cncls  23297  cnntr  23298  cnsscnp  23302  cmpsub  23423  2ndcsep  23482  1stcelcls  23484  lfinpfin  23547  locfincmp  23549  comppfsc  23555  txcn  23649  txlm  23671  xkohaus  23676  qtopres  23721  haushmphlem  23810  cmphmph  23811  connhmph  23812  reghmph  23816  nrmhmph  23817  ptcmpfi  23836  reghaus  23848  fbssfi  23860  fbun  23863  fbfinnfr  23864  isfildlem  23880  fgcl  23901  cfinfil  23916  supfil  23918  ufinffr  23952  fin1aufil  23955  cnpflf  24024  alexsubALTlem3  24072  alexsubALT  24074  cnextfvval  24088  cnextcn  24090  tmdgsum  24118  tgphaus  24140  tgpt1  24141  mettri  24377  blssexps  24451  blssex  24452  mopni3  24522  metss  24536  psmetutop  24595  dscmet  24600  tngngp3  24692  rectbntr0  24867  metnrmlem1a  24893  fsumcn  24907  lmmbr  25305  caubl  25355  caublcls  25356  bcthlem5  25375  bcth3  25378  ovolunlem1a  25544  ovoliunnul  25555  finiunmbl  25592  voliunlem1  25598  volsuplem  25603  volsup  25604  dyadmax  25646  itgfsum  25876  dvnadd  25979  cpnord  25985  dvnfre  26004  dvmptfsum  26027  dvlip  26046  fta1g  26223  plyco  26294  dgrcolem1  26327  dgrco  26329  dvnply2  26343  plydivex  26353  plyexmo  26369  aannenlem1  26384  aaliou3lem2  26399  dvntaylp  26427  taylthlem1  26429  ulmval  26437  cxpmul2  26745  cxpsqrtth  26786  scvxcvx  27043  jensenlem2  27045  jensen  27046  ppiub  27262  bcmono  27335  bpos1lem  27340  bposlem5  27346  gausslemma2dlem6  27430  lgsquad2lem2  27443  2lgslem3  27462  2lgs  27465  2sqnn  27497  addsqnreup  27501  2sqreultblem  27506  2sqreunnltblem  27509  dchrisumlem1  27547  dchrisum0flb  27568  pntpbnd1  27644  pntlemf  27663  qabvle  27683  qabvexp  27684  ostthlem2  27686  ostth2lem2  27692  sltval2  27715  sltsolem1  27734  negsprop  28081  mulsuniflem  28189  precsexlem6  28250  precsexlem7  28251  noseqind  28312  om2noseqlt  28319  n0addscl  28361  n0mulscl  28362  expsne0  28428  axeuclidlem  28991  axcontlem12  29004  umgrnloopv  29137  uhgredgrnv  29161  edglnl  29174  numedglnl  29175  usgruspgrb  29214  usgrnloopvALT  29232  usgredg2vlem2  29257  subupgr  29318  nbumgr  29378  uhgrnbgr0nb  29385  nbgr0edglem  29387  edgusgrnbfin  29404  nb3grprlem2  29412  uvtxnbgrvtx  29424  cplgrop  29468  cusgrfi  29490  fusgrmaxsize  29496  fusgrn0degnn0  29531  ewlkprop  29635  uspgr2wlkeq  29678  g0wlk0  29684  wlkreslem  29701  lfgriswlk  29720  upgrwlkdvde  29769  spthonepeq  29784  uhgrwkspth  29787  usgr2trlncl  29792  usgr2trlspth  29793  cyclnspth  29832  crctcshwlkn0lem3  29841  wwlksn  29866  wspthneq1eq2  29889  wwlksm1edg  29910  wwlksnred  29921  wwlksnextfun  29927  wwlksnextinj  29928  wwlksnextproplem3  29940  wspthsnonn0vne  29946  wspn0  29953  rusgrnumwwlk  30004  clwwlkccatlem  30017  umgrclwwlkge2  30019  clwlkclwwlklem2  30028  clwlkclwwlklem3  30029  clwwisshclwws  30043  clwwisshclwwsn  30044  clwwlkn1loopb  30071  wwlksext2clwwlk  30085  wwlksubclwwlk  30086  clwwlknonex2lem2  30136  upgr3v3e3cycl  30208  uhgr3cyclex  30210  upgr4cycl4dv4e  30213  eupth2lem3lem4  30259  eupth2lem3lem7  30262  eupth2  30267  eulerpath  30269  nfrgr2v  30300  frgr3vlem1  30301  3vfriswmgr  30306  1to2vfriswmgr  30307  1to3vfriswmgr  30308  3cyclfrgrrn1  30313  3cyclfrgrrn  30314  3cyclfrgrrn2  30315  4cycl2vnunb  30318  frgrncvvdeqlem2  30328  frgrncvvdeqlem8  30334  frgrncvvdeqlem9  30335  frgrwopreglem4a  30338  frgrwopreglem5lem  30348  frgrwopreglem5ALT  30350  frgrregorufr0  30352  frgr2wwlk1  30357  frgr2wwlkeqm  30359  fusgr2wsp2nb  30362  2wspmdisj  30365  frrusgrord  30369  numclwwlk1lem2f1  30385  numclwlk1  30399  frgrreggt1  30421  friendshipgt3  30426  hlim2  31220  elnlfn  31956  stle0i  32267  hstrbi  32294  spansncv2  32321  h1da  32377  fmptcof2  32673  xreceu  32888  domnprodn0  33261  1arithufdlem3  33553  1arithufdlem4  33554  tpr2rico  33872  hasheuni  34065  ismeas  34179  sseqp1  34376  rrvsum  34435  dstfrvunirn  34455  sgn3da  34522  signstfvc  34567  bnj607  34908  bnj1145  34985  bnj1204  35004  fineqvrep  35087  fisshasheq  35098  subgrwlk  35116  subfacp1lem6  35169  cvmlift2lem12  35298  cvmlift3lem4  35306  satfrnmapom  35354  sat1el2xp  35363  satffunlem2  35392  satffun  35393  mrsubvrs  35506  climuzcnv  35655  iprodefisumlem  35719  dfon2lem9  35772  linethru  36134  elhf2  36156  finminlem  36300  fnessref  36339  neibastop2lem  36342  fnemeet2  36349  nndivsub  36439  bj-xpnzex  36941  bj-elpwg  37034  bj-epelg  37050  mptsnunlem  37320  dissneqlem  37322  topdifinffinlem  37329  iooelexlt  37344  domalom  37386  fvineqsneq  37394  wl-exeq  37514  wl-ax11-lem3  37567  matunitlindflem1  37602  poimirlem22  37628  poimirlem26  37632  poimirlem28  37634  poimirlem29  37635  poimirlem32  37638  heicant  37641  ovoliunnfl  37648  voliunnfl  37650  volsupnfl  37651  cover2  37701  upixp  37715  sdclem2  37728  fdc  37731  seqpo  37733  metf1o  37741  mettrifi  37743  sstotbnd3  37762  heibor1lem  37795  heiborlem5  37801  heibor  37807  bfplem1  37808  elghomlem2OLD  37872  grpokerinj  37879  isrngo  37883  rngodm1dm2  37918  ispridl2  38024  exlimddvf  38107  lssatle  38996  4atexlemex4  40055  uzindd  41958  evl1gprodd  42098  sn-axprlem3  42234  redvmptabs  42368  sn-sup3d  42478  mzpsubst  42735  jm2.18  42976  wepwsolem  43030  oaabsb  43283  oacl2g  43319  ofoafg  43343  ofoaid1  43347  ofoaid2  43348  naddonnn  43384  iunrelexp0  43691  relexpmulg  43699  cnvtrclfv  43713  clsk1indlem3  44032  grucollcld  44255  inaex  44292  dvgrat  44307  radcnvrat  44309  csbxpgVD  44891  sineq0ALT  44934  relwf  44941  islptre  45574  iblspltprt  45928  stoweidlem2  45957  stoweidlem17  45972  stoweidlem21  45976  2reuimp0  47063  2reuimp  47064  afveu  47102  funbrafv  47107  ndmaovass  47155  afv2eu  47187  tz6.12c-afv2  47191  funop1  47232  f1oresf1o2  47240  fvmptrabdm  47242  nltle2tri  47262  2elfz2melfz  47267  fsummsndifre  47296  fsumsplitsndif  47297  fsummmodsndifre  47298  fsummmodsnunz  47299  elsetpreimafvssdm  47310  uniimaelsetpreimafv  47320  imasetpreimafvbijlemfv1  47327  iccpartiltu  47346  iccpartigtl  47347  iccpartleu  47352  iccpartgel  47353  iccpartrn  47354  iccpartiun  47358  icceuelpart  47360  iccpartnel  47362  fargshiftf  47364  fargshiftf1  47365  ichnfb  47389  elsprel  47399  prsprel  47411  sprsymrelfo  47421  paireqne  47435  sbcpr  47445  reupr  47446  fmtnoinf  47460  odz2prm2pw  47487  lighneallem4  47534  lighneal  47535  requad1  47546  requad2  47547  evensumeven  47631  even3prm2  47643  gbowgt5  47686  nnsum4primeseven  47724  nnsum4primesevenALTV  47725  bgoldbnnsum3prm  47728  bgoldbtbndlem2  47730  bgoldbtbndlem4  47732  bgoldbtbnd  47733  dfsclnbgr6  47781  uspgrimprop  47810  grimco  47817  isubgr3stgrlem6  47873  gricgrlic  47913  gpgedgvtx0  47953  clcllaw  48034  rngccatidALTV  48115  ringccatidALTV  48149  scmsuppss  48215  gsumlsscl  48224  ply1mulgsumlem2  48232  lincvalsc0  48266  linc0scn0  48268  lincdifsn  48269  linc1  48270  lincellss  48271  lincsum  48274  lincscm  48275  lincsumcl  48276  lcoss  48281  lincext3  48301  lindslinindimp2lem4  48306  lindslinindsimp2lem5  48307  lindslinindsimp2  48308  lindsrng01  48313  snlindsntor  48316  lincresunit3lem2  48325  lincresunit3  48326  islindeps2  48328  blengt1fldiv2p1  48442  2arymaptf1  48502  resum2sqorgt0  48558  reorelicc  48559  rrx2plordisom  48572  rrx2linest  48591  rrxsphere  48597  line2ylem  48600  itsclc0xyqsol  48617  itscnhlinecirc02p  48634  mo0sn  48663  thincn0eu  48831