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  581  animpimp2impd  847  4casesdan  1042  dedlema  1046  dedlemb  1047  sbiedvw  2101  mo4  2567  2moswapv  2630  2moswap  2645  2mosOLD  2651  2eu2  2654  pm2.61ne  3018  nelelne  3032  r19.21be  3231  rspcebdv  3559  2reu2  3837  csbie2df  4384  minel  4407  uneqdifeq  4433  raltpd  4726  ssunsn2  4771  opthprneg  4809  ssuni  4876  uniss2  4885  elpwuni  5048  intss2  5051  disjord  5075  elpw2g  5270  elssabg  5280  axprlem3OLD  5366  axprlem4OLD  5367  axprlem5OLD  5368  axprglem  5373  oteqex  5448  otsndisj  5467  otiunsndisj  5468  epelg  5525  wereu  5620  relop  5799  riinint  5921  sotri3  6087  unixpid  6242  reuop  6251  ordtr2  6362  ordsssuc2  6410  iotan0  6482  funopg  6526  fun  6696  fvmptnf  6964  fvn0ssdmfun  7020  eldmrexrnb  7038  fmptco  7076  fnressn  7105  fressnfv  7107  fprb  7142  fvtp2g  7147  fvtp3g  7148  fconst2g  7151  fntpb  7157  f1dom3el3dif  7217  f1ounsn  7220  isores3  7283  isoselem  7289  oprabv  7420  eloprabga  7469  sorpsscmpl  7681  difex2  7707  ordpwsuc  7759  ordsucun  7769  limuni3  7796  trom  7819  fo1stres  7961  poxp  8071  soxp  8072  xpord3inddlem  8097  soseq  8102  suppimacnv  8117  fsuppeq  8118  funsssuppss  8133  brtpos2  8175  frrlem8  8236  fpr2a  8245  onnseq  8277  smores  8285  smofvon2  8289  tfrlem1  8308  oacl  8463  omcl  8464  oecl  8465  oawordri  8478  oalimcl  8488  oaass  8489  oarec  8490  omwordri  8500  omeulem1  8510  omeulem2  8511  oeordi  8516  oeworde  8522  oeoelem  8527  nnacl  8540  nnmcl  8541  nnecl  8542  nnacom  8546  nnaass  8551  nnmsucr  8554  nnmordi  8560  omabs  8580  cofonr  8603  naddunif  8622  iiner  8729  elpmg  8783  fsetfcdm  8800  fsetprcnex  8802  pmss12g  8810  mapfvd  8820  f1domg  8911  ssdomg  8940  undom  8996  domtriord  9054  ssnnfi  9097  fnfi  9105  enfi  9114  php  9134  sdom1  9153  1sdom2dom  9157  fisseneq  9166  isinf  9168  dif1ennnALT  9180  findcard3  9186  frfi  9188  difinf  9214  imafiOLD  9219  iunfi  9246  fsuppunfi  9294  fsuppres  9299  ffsuppbi  9304  elfi2  9320  marypha1lem  9339  marypha1  9340  oiexg  9443  wemapso2  9461  harword  9471  brwdom  9475  unxpwdom  9497  en3lplem1  9524  inf3lemd  9539  inf3lem5  9544  cantnfval2  9581  cantnfle  9583  cantnflt  9584  cnfcom  9612  tcmin  9651  frr2  9675  r1sdom  9689  rankxplim3  9796  cardidm  9874  cardmin2  9914  infxpenlem  9926  fseqenlem1  9937  numacn  9962  alephordi  9987  iscard3  10006  alephinit  10008  carduniima  10009  iunfictbso  10027  dfac5  10042  dfac12lem3  10059  nnadju  10111  pwsdompw  10116  pwdjudom  10128  cflim2  10176  cfslb2n  10181  cofsmo  10182  cfsmolem  10183  cfcoflem  10185  alephsing  10189  infpssALT  10226  fin23lem34  10259  isf32lem2  10267  isf32lem10  10275  isf32lem12  10277  isfin1-2  10298  hsmexlem4  10342  axcc2lem  10349  domtriomlem  10355  axdc2lem  10361  axdc3lem2  10364  axdc3lem4  10366  axdc4lem  10368  axcclem  10370  ac6num  10392  ac6s  10397  zorn2lem7  10415  ttukeylem5  10426  imadomg  10447  iundom2g  10453  ondomon  10476  ficard  10478  konigthlem  10482  alephreg  10496  pwcfsdom  10497  cfpwsdom  10498  axregndlem1  10516  axregnd  10518  pwfseqlem3  10574  pwxpndom2  10579  pwxpndom  10580  pwdjundom  10581  inawinalem  10603  gchina  10613  wuncval2  10661  tsk0  10677  tskxpss  10686  inatsk  10692  tskuni  10697  gruina  10732  grothac  10744  addclpi  10806  addnidpi  10815  nqereu  10843  mulcanenq  10874  genpnnp  10919  nqpr  10928  prlem934  10947  reclem2pr  10962  suplem1pr  10966  supsrlem  11025  axpre-sup  11083  1re  11135  dedekindle  11301  00id  11312  receu  11786  sup3  12104  infrelb  12132  peano5nni  12168  nnindd  12185  nnaddcl  12188  zrevaddcl  12563  nzadd  12566  zdiv  12590  nneo  12604  zeo2  12607  nn0indd  12617  fzind  12618  fnn0ind  12619  fzindd  12622  uzwo  12852  lbzbi  12877  nn01to3  12882  qrevaddcl  12912  irradd  12914  irrmul  12915  ltsubrp  12971  ltaddrp  12972  xnn0xaddcl  13178  xnn0xadd0  13190  icoshft  13417  fzen  13486  elfzm11  13540  uzsplit  13541  elfzom1elp1fzo  13678  fzoopth  13708  injresinjlem  13736  injresinj  13737  modifeq2int  13886  modsumfzodifsn  13897  om2uzlti  13903  ssnn0fi  13938  fsuppmapnn0fiub0  13946  mptnn0fsuppr  13952  seqcaopr3  13990  seqf1olem2a  13993  seqf1o  13996  ser1const  14011  expadd  14057  expmul  14060  leexp1a  14128  faccl  14236  facdiv  14240  faclbnd  14243  faclbnd4lem4  14249  hasheqf1oi  14304  hashgadd  14330  hashinfxadd  14338  hashunx  14339  hashunsng  14345  elprchashprn2  14349  hashss  14362  hash1snb  14372  hashmap  14388  hashf1lem2  14409  hashf1  14410  seqcoll  14417  hashle2pr  14430  hashdmpropge2  14436  hashge3el3dif  14440  hash1to3  14445  fundmge2nop0  14455  fi1uzind  14460  brfi1indALT  14463  sswrd  14475  swrdnd2  14609  swrdnnn0nd  14610  swrdnd0  14611  swrdwrdsymb  14616  pfxnd0  14642  swrdswrdlem  14657  swrdswrd  14658  wrd2ind  14676  swrdccatin1  14678  swrdccatin2  14682  pfxccatin12lem2  14684  pfxccat3  14687  repsdf2  14731  repswswrd  14737  cshw0  14747  cshwcl  14751  cshwlen  14752  cshf1  14763  swrdco  14790  relexpsucnnl  14983  rtrclreclem3  15013  rtrclreclem4  15014  relexpindlem  15016  rtrclind  15018  shftlem  15021  caubnd  15312  reusq0  15418  rlimcld2  15531  o1dif  15583  climub  15615  climserle  15616  iseraltlem2  15636  sumss  15677  fsumzcl2  15692  fsummsnunz  15707  fsumsplitsnun  15708  fsum2d  15724  modfsummods  15747  fsumabs  15755  fsumrlim  15765  fsumo1  15766  fsumiun  15775  climcndslem1  15805  climcndslem2  15806  cvgrat  15839  clim2prod  15844  prodfn0  15850  prodfrec  15851  ntrivcvg  15853  prodmo  15892  fprodss  15904  fprodabs  15930  fprodn0  15935  fprod2d  15937  fprodefsum  16051  ruclem8  16195  ruclem9  16196  dvdsmod0  16218  dvds2ln  16249  dvdsaddre2b  16267  dvdslelem  16269  dvdsdivcl  16276  alzdvds  16280  mod2eq1n2dvds  16307  oddnn02np1  16308  nn0o1gt2  16341  nno  16342  sumeven  16347  sumodd  16348  pwp1fsum  16351  ndvdsadd  16370  bitsinv1  16402  sadcadd  16418  sadadd2  16420  saddisjlem  16424  smuval2  16442  smupvallem  16443  smu01lem  16445  smupval  16448  smueqlem  16450  smumullem  16452  gcddiv  16511  rplpwr  16518  nn0seqcvgd  16530  seq1st  16531  alginv  16535  algcvga  16539  algfx  16540  absprodnn  16578  isprm2  16642  isprm3  16643  prmind2  16645  maxprmfct  16670  prmdvdsexp  16676  pcmpt  16854  prmreclem4  16881  vdwmc2  16941  vdwlem10  16952  ramub2  16976  ramcl  16991  prmgaplem5  17017  prmgaplem8  17020  cshwshashlem1  17057  cshwshashlem3  17059  setsn0fun  17134  imasleval  17496  divsfval  17502  mreexexlem4d  17604  isssc  17778  initoeu1  17969  termoeu1  17976  istos  18373  chnfibg  18593  mgmcl  18602  sgrpidmnd  18698  frmdgsum  18821  smndex1mgm  18869  dfgrp3lem  19005  mhmmulg  19082  resghm2b  19200  gsumwrev  19332  elsymgbas  19340  symgextf1  19387  gsmsymgreqlem2  19397  gsmsymgreq  19398  odlem1  19501  odcl2  19531  gexlem1  19545  efgi2  19691  efginvrel2  19693  efgsrel  19700  cyggexb  19865  gsummulglem  19907  gsumzunsnd  19922  gsum2dlem2  19937  telgsums  19959  dmdprd  19966  dprdw  19978  ablfac1eulem  20040  srgpcomp  20190  rnghmmul  20420  nrhmzr  20505  lmodfopnelem1  20884  rmodislmodlem  20915  cnfldmulg  21393  cnfldexp  21394  nzerooringczr  21470  obslbs  21720  mplcoe1  22025  mplcoe3  22026  mplcoe5  22028  cply1mul  22271  coe1fzgsumdlem  22278  gsummoncoe1  22283  pf1ind  22330  evl1gsumdlem  22331  mat1dimcrng  22452  ma1repveval  22546  mulmarep1gsum2  22549  gsummatr01lem3  22632  cramerlem3  22664  decpmatmulsumfsupp  22748  mp2pm2mplem4  22784  pm2mpmhmlem1  22793  fvmptnn04if  22824  cayhamlem1  22841  fctop  22979  mretopd  23067  restopnb  23150  restdis  23153  tgcnp  23228  cncls2  23248  cncls  23249  cnntr  23250  cnsscnp  23254  cmpsub  23375  2ndcsep  23434  1stcelcls  23436  lfinpfin  23499  locfincmp  23501  comppfsc  23507  txcn  23601  txlm  23623  xkohaus  23628  qtopres  23673  haushmphlem  23762  cmphmph  23763  connhmph  23764  reghmph  23768  nrmhmph  23769  ptcmpfi  23788  reghaus  23800  fbssfi  23812  fbun  23815  fbfinnfr  23816  isfildlem  23832  fgcl  23853  cfinfil  23868  supfil  23870  ufinffr  23904  fin1aufil  23907  cnpflf  23976  alexsubALTlem3  24024  alexsubALT  24026  cnextfvval  24040  cnextcn  24042  tmdgsum  24070  tgphaus  24092  tgpt1  24093  mettri  24327  blssexps  24401  blssex  24402  mopni3  24469  metss  24483  psmetutop  24542  dscmet  24547  tngngp3  24631  rectbntr0  24808  metnrmlem1a  24834  fsumcn  24847  lmmbr  25235  caubl  25285  caublcls  25286  bcthlem5  25305  bcth3  25308  ovolunlem1a  25473  ovoliunnul  25484  finiunmbl  25521  voliunlem1  25527  volsuplem  25532  volsup  25533  dyadmax  25575  itgfsum  25804  dvnadd  25906  cpnord  25912  dvnfre  25929  dvmptfsum  25952  dvlip  25970  fta1g  26145  plyco  26216  dgrcolem1  26248  dgrco  26250  dvnply2  26264  plydivex  26274  plyexmo  26290  aannenlem1  26305  aaliou3lem2  26320  dvntaylp  26348  taylthlem1  26350  ulmval  26358  cxpmul2  26666  cxpsqrtth  26707  scvxcvx  26963  jensenlem2  26965  jensen  26966  ppiub  27181  bcmono  27254  bpos1lem  27259  bposlem5  27265  gausslemma2dlem6  27349  lgsquad2lem2  27362  2lgslem3  27381  2lgs  27384  2sqnn  27416  addsqnreup  27420  2sqreultblem  27425  2sqreunnltblem  27428  dchrisumlem1  27466  dchrisum0flb  27487  pntpbnd1  27563  pntlemf  27582  qabvle  27602  qabvexp  27603  ostthlem2  27605  ostth2lem2  27611  ltsval2  27634  ltssolem1  27653  negsprop  28041  mulsuniflem  28155  precsexlem6  28218  precsexlem7  28219  noseqind  28298  om2noseqlt  28305  n0addscl  28350  n0mulscl  28351  expsne0  28442  axeuclidlem  29045  axcontlem12  29058  umgrnloopv  29189  uhgredgrnv  29213  edglnl  29226  numedglnl  29227  usgruspgrb  29266  usgrnloopvALT  29284  usgredg2vlem2  29309  subupgr  29370  nbumgr  29430  uhgrnbgr0nb  29437  nbgr0edglem  29439  edgusgrnbfin  29456  nb3grprlem2  29464  uvtxnbgrvtx  29476  cplgrop  29520  cusgrfi  29542  fusgrmaxsize  29548  fusgrn0degnn0  29583  ewlkprop  29687  uspgr2wlkeq  29729  g0wlk0  29734  wlkreslem  29751  lfgriswlk  29770  upgrwlkdvde  29820  spthonepeq  29835  uhgrwkspth  29838  usgr2trlncl  29843  usgr2trlspth  29844  cyclnumvtx  29883  cyclnspth  29884  crctcshwlkn0lem3  29895  wwlksn  29920  wspthneq1eq2  29943  wwlksm1edg  29964  wwlksnred  29975  wwlksnextfun  29981  wwlksnextinj  29982  wwlksnextproplem3  29994  wspthsnonn0vne  30000  wspn0  30007  rusgrnumwwlk  30061  clwwlkccatlem  30074  umgrclwwlkge2  30076  clwlkclwwlklem2  30085  clwlkclwwlklem3  30086  clwwisshclwws  30100  clwwisshclwwsn  30101  clwwlkn1loopb  30128  wwlksext2clwwlk  30142  wwlksubclwwlk  30143  clwwlknonex2lem2  30193  upgr3v3e3cycl  30265  uhgr3cyclex  30267  upgr4cycl4dv4e  30270  eupth2lem3lem4  30316  eupth2lem3lem7  30319  eupth2  30324  eulerpath  30326  nfrgr2v  30357  frgr3vlem1  30358  3vfriswmgr  30363  1to2vfriswmgr  30364  1to3vfriswmgr  30365  3cyclfrgrrn1  30370  3cyclfrgrrn  30371  3cyclfrgrrn2  30372  4cycl2vnunb  30375  frgrncvvdeqlem2  30385  frgrncvvdeqlem8  30391  frgrncvvdeqlem9  30392  frgrwopreglem4a  30395  frgrwopreglem5lem  30405  frgrwopreglem5ALT  30407  frgrregorufr0  30409  frgr2wwlk1  30414  frgr2wwlkeqm  30416  fusgr2wsp2nb  30419  2wspmdisj  30422  frrusgrord  30426  numclwwlk1lem2f1  30442  numclwlk1  30456  frgrreggt1  30478  friendshipgt3  30483  hlim2  31278  elnlfn  32014  stle0i  32325  hstrbi  32352  spansncv2  32379  h1da  32435  fmptcof2  32745  sgn3da  32922  xreceu  32996  domnprodn0  33351  1arithufdlem3  33621  1arithufdlem4  33622  tpr2rico  34072  hasheuni  34245  ismeas  34359  sseqp1  34555  rrvsum  34614  dstfrvunirn  34635  signstfvc  34734  bnj607  35074  bnj1145  35151  bnj1204  35170  r1filim  35263  fineqvrep  35274  fineqvnttrclselem1  35281  onvf1odlem4  35304  fisshasheq  35313  subgrwlk  35330  subfacp1lem6  35383  cvmlift2lem12  35512  cvmlift3lem4  35520  satfrnmapom  35568  sat1el2xp  35577  satffunlem2  35606  satffun  35607  mrsubvrs  35720  climuzcnv  35869  iprodefisumlem  35938  dfon2lem9  35987  linethru  36351  elhf2  36373  finminlem  36516  fnessref  36555  neibastop2lem  36558  fnemeet2  36565  nndivsub  36655  mh-inf3f1  36739  bj-cbvew  36952  bj-xpnzex  37282  bj-elpwg  37375  bj-epelg  37391  bj-axseprep  37397  mptsnunlem  37668  dissneqlem  37670  topdifinffinlem  37677  iooelexlt  37692  domalom  37734  fvineqsneq  37742  wl-exeq  37873  matunitlindflem1  37951  poimirlem22  37977  poimirlem26  37981  poimirlem28  37983  poimirlem29  37984  poimirlem32  37987  heicant  37990  ovoliunnfl  37997  voliunnfl  37999  volsupnfl  38000  cover2  38050  upixp  38064  sdclem2  38077  fdc  38080  seqpo  38082  metf1o  38090  mettrifi  38092  sstotbnd3  38111  heibor1lem  38144  heiborlem5  38150  heibor  38156  bfplem1  38157  elghomlem2OLD  38221  grpokerinj  38228  isrngo  38232  rngodm1dm2  38267  ispridl2  38373  exlimddvf  38456  lssatle  39475  4atexlemex4  40533  uzindd  42431  evl1gprodd  42570  sn-axprlem3  42673  redvmptabs  42806  sn-sup3d  42951  mzpsubst  43194  jm2.18  43434  wepwsolem  43488  oaabsb  43740  oacl2g  43776  ofoafg  43800  ofoaid1  43804  ofoaid2  43805  naddonnn  43841  iunrelexp0  44147  relexpmulg  44155  cnvtrclfv  44169  clsk1indlem3  44488  grucollcld  44705  inaex  44742  dvgrat  44757  radcnvrat  44759  csbxpgVD  45338  sineq0ALT  45381  trfr  45407  relwf  45412  pwclaxpow  45429  omssaxinf2  45433  islptre  46067  iblspltprt  46419  stoweidlem2  46448  stoweidlem17  46463  stoweidlem21  46467  2reuimp0  47574  2reuimp  47575  afveu  47613  funbrafv  47618  ndmaovass  47666  afv2eu  47698  tz6.12c-afv2  47702  funop1  47743  f1oresf1o2  47751  fvmptrabdm  47753  nltle2tri  47773  2elfz2melfz  47778  fsummsndifre  47840  fsumsplitsndif  47841  fsummmodsndifre  47842  fsummmodsnunz  47843  elsetpreimafvssdm  47858  uniimaelsetpreimafv  47868  imasetpreimafvbijlemfv1  47875  iccpartiltu  47894  iccpartigtl  47895  iccpartleu  47900  iccpartgel  47901  iccpartrn  47902  iccpartiun  47906  icceuelpart  47908  iccpartnel  47910  fargshiftf  47912  fargshiftf1  47913  ichnfb  47937  elsprel  47947  prsprel  47959  sprsymrelfo  47969  paireqne  47983  sbcpr  47993  reupr  47994  fmtnoinf  48011  odz2prm2pw  48038  lighneallem4  48085  lighneal  48086  requad1  48110  requad2  48111  evensumeven  48195  even3prm2  48207  gbowgt5  48250  nnsum4primeseven  48288  nnsum4primesevenALTV  48289  bgoldbnnsum3prm  48292  bgoldbtbndlem2  48294  bgoldbtbndlem4  48296  bgoldbtbnd  48297  dfsclnbgr6  48346  grimco  48377  cycl3grtri  48435  isubgr3stgrlem6  48459  gricgrlic  48506  gpgedgvtx0  48549  gpgprismgr4cycllem3  48585  pgnbgreunbgrlem5  48611  clcllaw  48679  rngccatidALTV  48760  ringccatidALTV  48794  scmsuppss  48859  gsumlsscl  48868  ply1mulgsumlem2  48875  lincvalsc0  48909  linc0scn0  48911  lincdifsn  48912  linc1  48913  lincellss  48914  lincsum  48917  lincscm  48918  lincsumcl  48919  lcoss  48924  lincext3  48944  lindslinindimp2lem4  48949  lindslinindsimp2lem5  48950  lindslinindsimp2  48951  lindsrng01  48956  snlindsntor  48959  lincresunit3lem2  48968  lincresunit3  48969  islindeps2  48971  blengt1fldiv2p1  49081  2arymaptf1  49141  resum2sqorgt0  49197  reorelicc  49198  rrx2plordisom  49211  rrx2linest  49230  rrxsphere  49236  line2ylem  49239  itsclc0xyqsol  49256  itscnhlinecirc02p  49273  mo0sn  49303  thincn0eu  49918